proposition: Lemma mult_resp_ap_zero : forall x y : F, x [#] [0] -> y [#] [0] -> x[*]y [#] [0].
proof: Proof. intros x y Hx Hy. apply cring_mult_ap_zero with (f_rcpcl y Hy). astepl x. auto. astepl (x[*][1]). eapply eq_transitive_unfolded. 2: apply CRings.mult_assoc. algebra. Qed.
imports: CoRN.algebra.CRings