Make use of new small_add

1 files changed, 8 insertions, 14 deletions

diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
index 9a9ba8149..780a5de60 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v
@@ -58,24 +58,18 @@ Section WordByWordMontgomery.
     subst R; destruct (Z.pos r ^ Z.of_nat R_numlimbs) eqn:?; [ | reflexivity | ];
       lia.
   Qed.
-
-
-  (*****************************************************************************************)
-  (** TODO(jadep) FIXME: Fill these in, replacing [Axiom] with [Local Notation] *)
   Local Lemma small_add : forall n a b, small a -> small b -> small (@add n a b).
   Proof.
-    intros; apply Saturated.small_add; auto; try lia.
-    cbv [uweight].
-    rewrite ?Znat.Nat2Z.inj_succ, ?Z.pow_succ_r by lia.
-    try nia.
-  Admitted.
+    intros; apply Saturated.small_add; auto; lia.
+  Qed.
   Local Lemma small_add' : forall n a b, small a -> small b -> small (@add' n a b).
   Proof.
-    intros; apply Saturated.small_add; auto; try lia.
-    (*cbv [uweight].
-    rewrite !Znat.Nat2Z.inj_succ, !Z.pow_succ_r by lia.
-    try nia.*)
-  Admitted.
+    intros; apply Saturated.small_add; auto; lia.
+  Qed.
+
+
+  (*****************************************************************************************)
+  (** TODO(jadep) FIXME: Fill these in, replacing [Axiom] with [Local Notation] *)
   Local Notation conditional_subtract_cps := (@drop_high_cps R_numlimbs).
   (*Axiom conditional_subtract_cps : T (S R_numlimbs) -> forall {cpsT}, (T R_numlimbs -> cpsT) -> cpsT *)(* computes [arg - N] if [R <= arg], and drops high bit *)
   Local Notation conditional_subtract := conditional_subtract.