diff options
Diffstat (limited to 'src/Encoding')
| -rw-r--r-- | src/Encoding/EncodingTheorems.v | 2 | ||||
| -rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/Encoding/EncodingTheorems.v b/src/Encoding/EncodingTheorems.v index 52ac91ada..c6f48a0ab 100644 --- a/src/Encoding/EncodingTheorems.v +++ b/src/Encoding/EncodingTheorems.v @@ -2,7 +2,7 @@ Require Import Crypto.Spec.Encoding. Section EncodingTheorems. Context {A B : Type} {E : canonical encoding of A as B}. - + Lemma encoding_inj : forall x y, enc x = enc y -> x = y. Proof. intros. diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 7251ac1e6..41b75e216 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -24,7 +24,7 @@ Section SignBit. assert (m < 1)%Z by (apply Z2Nat.inj_lt; try omega; assumption). omega. + assert (0 < m)%Z as m_pos by (pose proof prime_ge_2 m prime_m; omega). - pose proof (FieldToZ_range x m_pos). + pose proof (FieldToZ_range x m_pos). destruct (FieldToZ x); auto. - destruct p; auto. - pose proof (Pos2Z.neg_is_neg p); omega. |