proposition: Lemma mult_lft_resp_ap : forall x y z : F, x [#] y -> z [#] [0] -> z[*]x [#] z[*]y.
proof: Proof. intros x y z H Hz. apply zero_minus_apart. unfold cg_minus in |- *. astepl (z[*]x[+]z[*][--]y). astepl (z[*] (x[+][--]y)). astepl (z[*] (x[-]y)). apply mult_resp_ap_zero; algebra. Qed.
imports: CoRN.algebra.CRings