Fill in admits for field with carry_add, carry_opp, and carry_sub

1 files changed, 28 insertions, 0 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 9cef5710d..50da3a683 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -490,6 +490,34 @@ Section CarryProofs.
       auto using carry_chain_valid,  mul_rep.
   Qed.
 
+  Lemma carry_sub_rep : forall coeff coeff_mod a b,
+    eq
+      (carry_sub carry_chain coeff coeff_mod a b)
+      (sub coeff coeff_mod a b).
+  Proof.
+    cbv [carry_sub carry_]; intros.
+    eapply carry_sequence_rep; auto using carry_chain_valid.
+    reflexivity.
+  Qed.
+
+  Lemma carry_add_rep : forall a b,
+    eq (carry_add carry_chain a b) (add a b).
+  Proof.
+    cbv [carry_add carry_]; intros.
+    eapply carry_sequence_rep; auto using carry_chain_valid.
+    reflexivity.
+  Qed.
+
+  Print carry_opp.
+  Lemma carry_opp_rep : forall coeff coeff_mod a,
+    eq
+      (carry_opp carry_chain coeff coeff_mod a)
+      (opp coeff coeff_mod a).
+  Proof.
+    cbv [carry_opp opp]; intros.
+    apply carry_sub_rep.
+  Qed.
+
 End CarryProofs.
 
 Hint Rewrite @length_carry_and_reduce @length_carry : distr_length.