diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-02-21 18:01:18 -0500 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
| commit | f5c6a57c1453249aac448a33ac3443e45a0d3222 (patch) | |
| tree | 72919ee54472c746feab4b51898095ae5caad768 /src/Algebra/IntegralDomain.v | |
| parent | c1c764ead6291e25f6da3508f1ae2b46c1e574d4 (diff) | |
rewrite ExtendedCoordinates, fix Ed25519
Diffstat (limited to 'src/Algebra/IntegralDomain.v')
| -rw-r--r-- | src/Algebra/IntegralDomain.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v index 066886e83..8110ad5cd 100644 --- a/src/Algebra/IntegralDomain.v +++ b/src/Algebra/IntegralDomain.v @@ -19,7 +19,6 @@ Module IntegralDomain. Module _LargeCharacteristicReflective. Section ReflectiveNsatzSideConditionProver. Import BinInt BinNat BinPos. - Lemma N_one_le_pos p : (N.one <= N.pos p)%N. Admitted. Context {R eq zero one opp add sub mul} {ring:@Algebra.ring R eq zero one opp add sub mul} {zpzf:@Algebra.is_zero_product_zero_factor R eq zero mul}. @@ -50,8 +49,9 @@ Module IntegralDomain. Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c. Proof. + Set Printing All. induction c; simpl CtoZ; simpl denote; - repeat (rewrite_hyp ?*; Ring.push_homomorphism constr:(of_Z)); reflexivity. + repeat (rewrite_hyp ?* || Ring.push_homomorphism constr:(of_Z)); reflexivity. Qed. (* TODO: move *) |