From bc46f85d089099aa92d3ea12555e6510cbcffa78 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 12 Feb 2017 19:16:26 -0500 Subject: change weierstrass spec, prove most cases of associativity --- src/Algebra/Ring.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/Algebra') diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v index 2d8061ddc..3752c7562 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -60,6 +60,15 @@ Section Ring. eapply Group.cancel_left, mul_opp_l. Qed. + Lemma sub_zero_iff x y : x - y = 0 <-> x = y. + Proof. + split; intro E. + { rewrite <-(right_identity y), <- E, ring_sub_definition. + rewrite commutative, <-associative, commutative. + rewrite left_inverse, left_identity. reflexivity. } + { rewrite E, ring_sub_definition, right_inverse; reflexivity. } + Qed. + Lemma neq_sub_neq_zero x y (Hxy:x<>y) : x-y <> 0. Proof. intro Hsub. apply Hxy. rewrite <-(left_identity y), <-Hsub, ring_sub_definition. -- cgit v1.2.3