Copy bounds

```bash
$ pushd src/SpecificGen; pushd
$ pushd && for i in *.json; do ./copy_bounds.sh $i; done && pushd
```

6 files changed, 192 insertions, 270 deletions

diff --git a/src/SpecificGen/GF2213_32ExtendedAddCoordinates.v b/src/SpecificGen/GF2213_32ExtendedAddCoordinates.v
index 3ab6d9ada..0e2937fcc 100644
--- a/src/SpecificGen/GF2213_32ExtendedAddCoordinates.v
+++ b/src/SpecificGen/GF2213_32ExtendedAddCoordinates.v
@@ -10,58 +10,45 @@ Require Import Crypto.SpecificGen.GF2213_32.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 
 Definition edwards_extended_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         add sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
 Definition edwards_extended_carry_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         carry_add carry_sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-Print edwards_extended_add_coordinates.
 
 Create HintDb edwards_extended_add_coordinates_correct discriminated.
-Section noncarry.
-  Local Existing Instance field2213_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F2213_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_F2213_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_F2213_32_decode))
+Local Existing Instance field2213_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F2213_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_F2213_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_F2213_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End noncarry.
-Section carry.
-  Local Existing Instance carry_field2213_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F2213_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_carry_F2213_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_carry_F2213_32_decode))
+Lemma edwards_extended_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
+Local Existing Instance carry_field2213_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F2213_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_carry_F2213_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_carry_F2213_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_carry_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_carry_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End carry.
+Lemma edwards_extended_carry_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_carry_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
 
 Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q :
   Tuple.fieldwise
diff --git a/src/SpecificGen/GF2519_32ExtendedAddCoordinates.v b/src/SpecificGen/GF2519_32ExtendedAddCoordinates.v
index 32ac4258f..6eec2524e 100644
--- a/src/SpecificGen/GF2519_32ExtendedAddCoordinates.v
+++ b/src/SpecificGen/GF2519_32ExtendedAddCoordinates.v
@@ -10,58 +10,45 @@ Require Import Crypto.SpecificGen.GF2519_32.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 
 Definition edwards_extended_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         add sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
 Definition edwards_extended_carry_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         carry_add carry_sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-Print edwards_extended_add_coordinates.
 
 Create HintDb edwards_extended_add_coordinates_correct discriminated.
-Section noncarry.
-  Local Existing Instance field2519_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F2519_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_F2519_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_F2519_32_decode))
+Local Existing Instance field2519_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F2519_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_F2519_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_F2519_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End noncarry.
-Section carry.
-  Local Existing Instance carry_field2519_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F2519_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_carry_F2519_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_carry_F2519_32_decode))
+Lemma edwards_extended_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
+Local Existing Instance carry_field2519_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F2519_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_carry_F2519_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_carry_F2519_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_carry_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_carry_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End carry.
+Lemma edwards_extended_carry_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_carry_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
 
 Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q :
   Tuple.fieldwise
diff --git a/src/SpecificGen/GF25519_32ExtendedAddCoordinates.v b/src/SpecificGen/GF25519_32ExtendedAddCoordinates.v
index 0fdab1b24..d4cd36b5c 100644
--- a/src/SpecificGen/GF25519_32ExtendedAddCoordinates.v
+++ b/src/SpecificGen/GF25519_32ExtendedAddCoordinates.v
@@ -10,58 +10,45 @@ Require Import Crypto.SpecificGen.GF25519_32.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 
 Definition edwards_extended_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         add sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
 Definition edwards_extended_carry_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         carry_add carry_sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-Print edwards_extended_add_coordinates.
 
 Create HintDb edwards_extended_add_coordinates_correct discriminated.
-Section noncarry.
-  Local Existing Instance field25519_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_F25519_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_F25519_32_decode))
+Local Existing Instance field25519_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_F25519_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_F25519_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End noncarry.
-Section carry.
-  Local Existing Instance carry_field25519_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_carry_F25519_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_carry_F25519_32_decode))
+Lemma edwards_extended_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
+Local Existing Instance carry_field25519_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_carry_F25519_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_carry_F25519_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_carry_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_carry_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End carry.
+Lemma edwards_extended_carry_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_carry_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
 
 Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q :
   Tuple.fieldwise
diff --git a/src/SpecificGen/GF25519_64ExtendedAddCoordinates.v b/src/SpecificGen/GF25519_64ExtendedAddCoordinates.v
index 3c6f47518..5e3319ccb 100644
--- a/src/SpecificGen/GF25519_64ExtendedAddCoordinates.v
+++ b/src/SpecificGen/GF25519_64ExtendedAddCoordinates.v
@@ -10,58 +10,45 @@ Require Import Crypto.SpecificGen.GF25519_64.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 
 Definition edwards_extended_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         add sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
 Definition edwards_extended_carry_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         carry_add carry_sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-Print edwards_extended_add_coordinates.
 
 Create HintDb edwards_extended_add_coordinates_correct discriminated.
-Section noncarry.
-  Local Existing Instance field25519_64.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_64_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_F25519_64_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_F25519_64_decode))
+Local Existing Instance field25519_64.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F25519_64_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_F25519_64_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_F25519_64_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End noncarry.
-Section carry.
-  Local Existing Instance carry_field25519_64.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_64_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_carry_F25519_64_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_carry_F25519_64_decode))
+Lemma edwards_extended_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
+Local Existing Instance carry_field25519_64.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F25519_64_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_carry_F25519_64_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_carry_F25519_64_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_carry_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_carry_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End carry.
+Lemma edwards_extended_carry_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_carry_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
 
 Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q :
   Tuple.fieldwise
diff --git a/src/SpecificGen/GF41417_32ExtendedAddCoordinates.v b/src/SpecificGen/GF41417_32ExtendedAddCoordinates.v
index f75f179e8..2223b482a 100644
--- a/src/SpecificGen/GF41417_32ExtendedAddCoordinates.v
+++ b/src/SpecificGen/GF41417_32ExtendedAddCoordinates.v
@@ -10,58 +10,45 @@ Require Import Crypto.SpecificGen.GF41417_32.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 
 Definition edwards_extended_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         add sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
 Definition edwards_extended_carry_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         carry_add carry_sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-Print edwards_extended_add_coordinates.
 
 Create HintDb edwards_extended_add_coordinates_correct discriminated.
-Section noncarry.
-  Local Existing Instance field41417_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F41417_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_F41417_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_F41417_32_decode))
+Local Existing Instance field41417_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F41417_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_F41417_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_F41417_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End noncarry.
-Section carry.
-  Local Existing Instance carry_field41417_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F41417_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_carry_F41417_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_carry_F41417_32_decode))
+Lemma edwards_extended_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
+Local Existing Instance carry_field41417_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F41417_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_carry_F41417_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_carry_F41417_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_carry_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_carry_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End carry.
+Lemma edwards_extended_carry_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_carry_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
 
 Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q :
   Tuple.fieldwise
diff --git a/src/SpecificGen/GF5211_32ExtendedAddCoordinates.v b/src/SpecificGen/GF5211_32ExtendedAddCoordinates.v
index f1dcad937..b5a67ed4f 100644
--- a/src/SpecificGen/GF5211_32ExtendedAddCoordinates.v
+++ b/src/SpecificGen/GF5211_32ExtendedAddCoordinates.v
@@ -10,58 +10,45 @@ Require Import Crypto.SpecificGen.GF5211_32.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 
 Definition edwards_extended_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         add sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
 Definition edwards_extended_carry_add_coordinates td P Q :=
-Eval cbv iota beta delta [
-       Extended.add_coordinates
-         carry_add carry_sub mul
-     ] in
     (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-Print edwards_extended_add_coordinates.
 
 Create HintDb edwards_extended_add_coordinates_correct discriminated.
-Section noncarry.
-  Local Existing Instance field5211_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F5211_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_F5211_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_F5211_32_decode))
+Local Existing Instance field5211_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_F5211_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_F5211_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_F5211_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End noncarry.
-Section carry.
-  Local Existing Instance carry_field5211_32.
-  Hint Rewrite
-        (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F5211_32_decode))
-        (Ring.homomorphism_add(H1             :=homomorphism_carry_F5211_32_decode))
-        (Ring.homomorphism_sub(H1             :=homomorphism_carry_F5211_32_decode))
+Lemma edwards_extended_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ add sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
+Local Existing Instance carry_field5211_32.
+Hint Rewrite
+     (Ring.homomorphism_mul(is_homomorphism:=homomorphism_carry_F5211_32_decode))
+     (Ring.homomorphism_add(H1             :=homomorphism_carry_F5211_32_decode))
+     (Ring.homomorphism_sub(H1             :=homomorphism_carry_F5211_32_decode))
   : edwards_extended_add_coordinates_correct.
-  Lemma edwards_extended_carry_add_coordinates_correct td P Q :
-    Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
-    = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
-  Proof.
-    change (edwards_extended_carry_add_coordinates td P Q)
-    with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
-    destruct_head' prod.
-    simpl.
-    rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
-    reflexivity.
-  Qed.
-End carry.
+Lemma edwards_extended_carry_add_coordinates_correct td P Q :
+  Tuple.map (n:=4) decode (edwards_extended_carry_add_coordinates td P Q)
+  = (@ExtendedCoordinates.Extended.add_coordinates _ F.add F.sub F.mul (decode td) (Tuple.map (n:=4) decode P) (Tuple.map (n:=4) decode Q)).
+Proof.
+  change (edwards_extended_carry_add_coordinates td P Q)
+  with (@ExtendedCoordinates.Extended.add_coordinates _ carry_add carry_sub mul td P Q).
+  destruct_head' prod.
+  simpl.
+  rewrite_strat topdown hints edwards_extended_add_coordinates_correct.
+  reflexivity.
+Qed.
 
 Lemma fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry td P Q :
   Tuple.fieldwise