diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-23 11:05:06 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-23 11:05:06 -0700 |
| commit | dbcbf49132215abf83fd21b14f3fd542ad382172 (patch) | |
| tree | 948bd9fb26adccb9a7c9bd4db098f6c5b3f0e3ad /src | |
| parent | 88432d03659b37f822d1b90edc5b48360495bc95 (diff) | |
Rename the nonzero lemma to an iff lemma
Diffstat (limited to 'src')
| -rw-r--r-- | src/Algebra.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index eacc2b8bb..cb7265532 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -426,12 +426,14 @@ Module IntegralDomain. 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. + Lemma mul_nonzero_nonzero_iff (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. } + split. + { intro H0; split; intro H1; apply H0; rewrite H1. + { apply Ring.mul_0_r. } + { apply Ring.mul_0_l. } } + { intros [? ?] ?; edestruct mul_nonzero_nonzero_cases; eauto with nocore. } Qed. Global Instance Integral_domain : |