Add mul_nonzero_nonzero_and to Algebra.v

1 files changed, 9 insertions, 1 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 6dc188e2c..eacc2b8bb 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -420,12 +420,20 @@ Module IntegralDomain.
     Context {T eq zero one opp add sub mul} `{@integral_domain T eq zero one opp add sub mul}.
 
     Lemma mul_nonzero_nonzero_cases (x y : T)
-      : eq (mul x  y) zero -> eq x zero \/ eq y zero.
+      : eq (mul x y) zero -> eq x zero \/ eq y zero.
     Proof.
       pose proof mul_nonzero_nonzero x y.
       destruct (eq_dec x zero); destruct (eq_dec y zero); intuition.
     Qed.
 
+    Lemma mul_nonzero_nonzero_and (x y : T)
+      : ~eq (mul x y) zero -> ~eq x zero /\ ~eq y zero.
+    Proof.
+      intro H0; split; intro H1; apply H0; rewrite H1.
+      { apply Ring.mul_0_r. }
+      { apply Ring.mul_0_l. }
+    Qed.
+
     Global Instance Integral_domain :
       @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops
                                        Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring.