proposition: Lemma mult_resp_neq_zero : forall x y : F, x[~=][0] -> y[~=][0] -> x[*]y[~=][0].
proof: Proof. intros x y Hx Hy. cut (~ Not (x [#] [0])). intro H. cut (~ Not (y [#] [0])). intro H0. apply notnot_ap_imp_neq. cut (x [#] [0] -> y [#] [0] -> x[*]y [#] [0]). intro H1. intro. apply H0; intro H3. apply H; intro H4. apply H2; auto. intros; apply mult_resp_ap_zero; auto. apply neq_imp_notnot_ap; auto. apply neq_imp_notnot_ap; auto. Qed.
imports: CoRN.algebra.CRings