proposition: Lemma mult_rht_resp_ap : forall x y z : F, x [#] y -> z [#] [0] -> x[*]z [#] y[*]z.
proof: Proof. intros x y z H Hz. astepl (z[*]x). astepr (z[*]y). apply mult_lft_resp_ap; assumption. Qed.
imports: CoRN.algebra.CRings