Remove some admitted lemmas

1 files changed, 1 insertions, 30 deletions

diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v
index 092630eab..e84c8d083 100644
--- a/src/Arithmetic/Saturated/MontgomeryAPI.v
+++ b/src/Arithmetic/Saturated/MontgomeryAPI.v
@@ -383,23 +383,9 @@ Section API.
       eauto using small_add, small_join0.
     Qed.
 
-    Lemma small_add_S2 n a b :
-      (2 <= bound) ->
-      small a -> small b -> small (@add_S2 n a b).
-    Proof.
-      intros. pose_all.
-      cbv [add_cps add add_S2 Let_In].
-      autorewrite with uncps push_id.
-      (*apply Positional.small_sat_add.*)
-    Admitted.
-
     Lemma small_left_tl n (v:T (S n)) : small v -> small (left_tl v).
     Proof. cbv [small]. auto using Tuple.In_to_list_left_tl. Qed.
 
-    Lemma small_divmod n (p: T (S n)) (Hsmall : small p) :
-      left_hd p = eval p / uweight bound n /\ eval (left_tl p) = eval p mod (uweight bound n).
-    Admitted.
-
     Lemma eval_drop_high n v :
       small v -> eval (@drop_high n v) = eval v mod (uweight bound n).
     Proof.
@@ -482,21 +468,6 @@ Section API.
      apply small_drop_high,  @B.Positional.small_sat_add; omega.
    Qed.
 
-   (* TODO : remove if unneeded when all admits are proven
-    Lemma small_highest_zero_iff {n} (p: T (S n)) (Hsmall : small p) :
-      (left_hd p = 0 <-> eval p < uweight bound n).
-    Proof.
-      destruct (small_divmod _ p Hsmall) as [Hdiv Hmod].
-      pose proof Hsmall as Hsmalltl. apply eval_small in Hsmall.
-      apply small_left_tl, eval_small in Hsmalltl. rewrite Hdiv.
-      rewrite (Z.div_small_iff (eval p) (uweight bound n))
-        by auto using uweight_nonzero.
-      split; [|intros; left; omega].
-      let H := fresh "H" in intro H; destruct H; [|omega].
-      omega.
-    Qed.
-    *)
-
     Lemma map2_zselect n cond x y :
       Tuple.map2 (n:=n) (Z.zselect cond) x y = if dec (cond = 0) then x else y.
     Proof.
@@ -632,4 +603,4 @@ Section API.
     Qed.
   End Proofs.
 End API.
-Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id add_S1_id add_S2_id sub_then_maybe_add_id conditional_sub_id : uncps.
\ No newline at end of file
+Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id add_S1_id add_S2_id sub_then_maybe_add_id conditional_sub_id : uncps.