proposition: Lemma mult_resp_neq : forall x y z : F, x[~=]y -> z[~=][0] -> x[*]z[~=]y[*]z.
proof: Proof. intros x y z H Hz. generalize (neq_imp_notnot_ap _ _ _ H). generalize (neq_imp_notnot_ap _ _ _ Hz). generalize (mult_rht_resp_ap x y z). intros H1 H2 H3. apply notnot_ap_imp_neq. intro H4. apply H2; intro. apply H3; intro. apply H4. auto. Qed.
imports: CoRN.algebra.CRings