proposition: Lemma div_resp_ap_zero_rev : forall (x y : F) y_, x [#] [0] -> (x[/] y[//]y_) [#] [0].
proof: Proof. intros x y nzy Hx. unfold cf_div in |- *. apply mult_resp_ap_zero. assumption. apply f_rcpcl_resp_ap_zero. Qed.
imports: CoRN.algebra.CRings