proposition: Lemma div_div2 : forall (x y z : F) y_ z_ yz_, (x[/] y[/] z[//]z_[//]yz_) [=] (x[*]z[/] y[//]y_).
proof: Proof. intros x y z nzy nzz nzyz. unfold cf_div in |- *. astepr (x[*] (z[*]f_rcpcl y nzy)). apply mult_wdr. cut (f_rcpcl z nzz [#] [0]). intro nzrz. apply eq_transitive_unfolded with (f_rcpcl y nzy[*]f_rcpcl (f_rcpcl z nzz) nzrz). apply f_rcpcl_mult. astepr (f_rcpcl y nzy[*]z). apply mult_wdr. apply f_rcpcl_f_rcpcl. apply f_rcpcl_resp_ap_zero. Qed.
imports: CoRN.algebra.CRings