diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-06-20 15:07:03 -0400 |
| commit | 0ae5f6871b29d20f48b5df6dab663b5a44162d01 (patch) | |
| tree | 33b11090af2555a91a593f9b919edf83c71557cd /src/Encoding/ModularWordEncodingTheorems.v | |
| parent | a0bdb14300aa57eed684992a23a57fd319ef97c0 (diff) | |
remove trailing whitespace from src/
Diffstat (limited to 'src/Encoding/ModularWordEncodingTheorems.v')
| -rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |