proposition: Lemma div_wd : forall (x x' y y' : F) y_ y'_, x [=] x' -> y [=] y' -> (x[/] y[//]y_) [=] (x'[/] y'[//]y'_).
proof: Proof. intros x x' y y' nzy nzy' H H0. unfold cf_div in |- *. cut (f_rcpcl y nzy [=] f_rcpcl y' nzy'). intro H1. algebra. apply f_rcpcl_wd. assumption. Qed.
imports: CoRN.algebra.CRings