From c5b008e59cf53e9bd0c2efda8c680b3ffba58569 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 23 Jun 2016 15:52:48 -0700 Subject: Improve some tactics and lemmas --- src/Algebra.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/Algebra.v') 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. -- cgit v1.2.3