[field_algebra] now knows that 0 <> -0 is false

1 files changed, 7 insertions, 1 deletions

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}.