diff options
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 8 |
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}. |