proposition: Lemma f_rcpcl_mult : forall (y z : F) y_ z_ yz_, f_rcpcl (y[*]z) yz_ [=] f_rcpcl y y_[*]f_rcpcl z z_.
proof: Proof. intros y z nzy nzz nzyz. apply mult_cancel_lft with (y[*]z). assumption. astepl ([1]:F). astepr (y[*]z[*] (f_rcpcl z nzz[*]f_rcpcl y nzy)). astepr (y[*] (z[*] (f_rcpcl z nzz[*]f_rcpcl y nzy))). astepr (y[*] (z[*]f_rcpcl z nzz[*]f_rcpcl y nzy)). astepr (y[*] ([1][*]f_rcpcl y nzy)). astepr (y[*]f_rcpcl y nzy). Step_final ([1]:F). Qed.
imports: CoRN.algebra.CRings