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