1 files changed, 7 insertions, 0 deletions
diff --git a/src/Galois/Galois.v b/src/Galois/Galois.v
index 3ee86e4e4..4fd151d36 100644
--- a/src/Galois/Galois.v
+++ b/src/Galois/Galois.v
@@ -53,6 +53,13 @@ Module Galois (M: Modulus).
               apply prime_ge_2 in p; intuition).
   Defined.
 
+  Lemma GFone_nonzero : GFone <> GFzero.
+  Proof.
+    unfold GFone, GFzero.
+    intuition; solve_by_inversion.
+  Qed.
+  Hint Resolve GFone_nonzero.
+
   Definition GFplus(x y: GF): GF.
     exists ((x + y) mod modulus);
     abstract (rewrite Zmod_mod; trivial).