proposition: Lemma mult_eq_zero : forall x y : F, x[~=][0] -> x[*]y [=] [0] -> y [=] [0].
proof: Proof. intros x y Hx Hxy. apply not_ap_imp_eq. intro H. elim (eq_imp_not_neq _ _ _ Hxy). apply mult_resp_neq_zero. assumption. apply ap_imp_neq. assumption. Qed.
imports: CoRN.algebra.CRings