proposition: Lemma mult_of_divs : forall (x y p q : F) y_ q_ yq_, (x[*]p[/] y[*]q[//]yq_) [=] (x[/] y[//]y_) [*] (p[/] q[//]q_).
proof: Proof. intros x y p q nzy nzq nzyq. unfold cf_div in |- *. astepl (x[*] (p[*]f_rcpcl (y[*]q) nzyq)). astepr (x[*] (f_rcpcl y nzy[*] (p[*]f_rcpcl q nzq))). apply mult_wdr. astepr (f_rcpcl y nzy[*]p[*]f_rcpcl q nzq). astepr (p[*]f_rcpcl y nzy[*]f_rcpcl q nzq). astepr (p[*] (f_rcpcl y nzy[*]f_rcpcl q nzq)). apply mult_wdr. apply f_rcpcl_mult. Qed.
imports: CoRN.algebra.CRings