diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-09-05 12:35:38 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-09-06 11:20:59 -0400 |
| commit | ebb83ddb57aa8da5dbaae11de69c2fdc1a3e8c97 (patch) | |
| tree | f595a933abd65fde2632e7929e3c341cceba9bd9 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | c00aa881d043c40f6dda4c304c28ef199064f143 (diff) | |
Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleaning up freeze-related organization and definitions along the way
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 3b04eda2f..561c1ae81 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -447,16 +447,6 @@ Section CarryProofs. apply IHis; auto using in_cons. Qed. - Lemma carry_full_preserves_rep : forall us x, - rep us x -> rep (carry_full us) x. - Proof. - unfold carry_full; intros. - apply carry_sequence_rep; auto. - unfold full_carry_chain; apply make_chain_lt. - Qed. - - Opaque carry_full. - Context `{cc : CarryChain limb_widths}. Lemma carry_mul_rep : forall us vs x y, rep us x -> rep vs y -> |