diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-02-12 19:16:26 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-03-02 13:37:14 -0500 |
commit | bc46f85d089099aa92d3ea12555e6510cbcffa78 (patch) | |
tree | cac00ea0f50bc3b7ba101181161ab76dbd55e797 /src/Algebra | |
parent | e8fab6b839e19da231333ca8173bbb2a3d8a4033 (diff) |
change weierstrass spec, prove most cases of associativity
Diffstat (limited to 'src/Algebra')
-rw-r--r-- | src/Algebra/Ring.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |