From 0ae5f6871b29d20f48b5df6dab663b5a44162d01 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 20 Jun 2016 15:07:03 -0400 Subject: remove trailing whitespace from src/ --- src/Encoding/EncodingTheorems.v | 2 +- src/Encoding/ModularWordEncodingTheorems.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Encoding') 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. -- cgit v1.2.3