diff options
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 28 |
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. |