From 2f804f60377f36cbaa5bb0447a8c185626c540d9 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Thu, 23 Jun 2016 12:04:04 -0700
Subject: [field_algebra] now knows that 0 <> -0 is false

---
 src/Algebra.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'src/Algebra.v')

diff --git a/src/Algebra.v b/src/Algebra.v
index 5cb97f488..baa676b64 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -613,7 +613,13 @@ Ltac field_algebra :=
   try solve
       [neq01
       |trivial
-      |apply Ring.opp_nonzero_nonzero;trivial].
+      |apply Ring.opp_nonzero_nonzero;trivial
+      |match goal with
+       | [ H : not (?eq ?zero (?opp ?zero)) |- _ ]
+         => exfalso; apply H; nsatz
+       | [ H : not (?eq (?opp ?zero) ?zero) |- _ ]
+         => exfalso; apply H; nsatz
+       end].
 
 Section Example.
   Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
-- 
cgit v1.2.3