diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-23 15:52:48 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-23 15:52:48 -0700 |
| commit | c5b008e59cf53e9bd0c2efda8c680b3ffba58569 (patch) | |
| tree | 98ee674ca7ed627c69d3637be574610492902076 /src/Algebra.v | |
| parent | 93716330e8fcdb1cc69887eced3bdf5cc178f5ae (diff) | |
Improve some tactics and lemmas
Diffstat (limited to 'src/Algebra.v')
| -rw-r--r-- | src/Algebra.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index e12f68549..15e0bcd38 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -658,9 +658,10 @@ Ltac field_algebra := |apply Ring.opp_nonzero_nonzero;trivial]. Section ExtraLemmas. - Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. + Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}. Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div. Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. Lemma only_two_square_roots' x y : x * x = y * y -> x <> y -> x <> opp y -> False. Proof. |