Reworked square root theorems to prove they are valid iff a square root exists, not just if one exists.

1 files changed, 13 insertions, 0 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index fd903825e..d23a13e1d 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -637,6 +637,19 @@ Module Field.
         apply zero_neq_one. assumption.
     Qed.
 
+    Lemma mul_cancel_l_iff : forall x y, y <> 0 ->
+                                         (x * y = y <-> x = one).
+    Proof.
+      intros.
+      split; intros.
+      + rewrite <-(right_multiplicative_inverse y) by assumption.
+        rewrite <-H1 at 1; rewrite <-associative.
+        rewrite right_multiplicative_inverse by assumption.
+        rewrite right_identity.
+        reflexivity.
+      + rewrite H1; apply left_identity.
+    Qed.
+
     Require Coq.setoid_ring.Field_theory.
     Lemma field_theory_for_stdlib_tactic : Field_theory.field_theory 0 1 add mul sub opp div inv eq.
     Proof.