proposition: Lemma div_div : forall (x y z : F) y_ z_ yz_, ((x[/] y[//]y_) [/] z[//]z_) [=] (x[/] y[*]z[//]yz_).
proof: Proof. intros x y z nzy nzz nzyz. unfold cf_div in |- *. astepl (x[*] (f_rcpcl y nzy[*]f_rcpcl z nzz)). apply mult_wdr. apply eq_symmetric_unfolded. apply f_rcpcl_mult. Qed.
imports: CoRN.algebra.CRings