proposition: Lemma div_strext : forall (x x' y y' : F) y_ y'_, (x[/] y[//]y_) [#] (x'[/] y'[//]y'_) -> x [#] x' or y [#] y'.
proof: Proof. intros x x' y y' Hy Hy' H. unfold cf_div in H. elim (cs_bin_op_strext F cr_mult _ _ _ _ H). auto. intro H1. right. unfold f_rcpcl in H1. exact (pfstrx _ _ _ _ _ _ H1). Qed.
imports: CoRN.algebra.CRings