proposition: Lemma div_semi_sym : forall (x y z : F) y_ z_, ((x[/] y[//]y_) [/] z[//]z_) [=] ((x[/] z[//]z_) [/] y[//]y_).
proof: Proof. intros. unfold cf_div in |- *. astepl (x[*] ((f_rcpcl y y_) [*] (f_rcpcl z z_))). Step_final (x[*] ((f_rcpcl z z_) [*] (f_rcpcl y y_))). Qed.
imports: CoRN.algebra.CRings