proposition: Lemma part_function_div_strext : forall x y Hx Hy, (F x (prj1 X _ _ _ Hx) [/] _[//]Ext2R x (prj2 X _ _ _ Hx)) [#] (F y (prj1 X _ _ _ Hy) [/] _[//]Ext2R y (prj2 X _ _ _ Hy)) -> x [#] y.
proof: Proof. intros x y Hx Hy H. elim (div_strext _ _ _ _ _ _ _ H); intro H1; exact (pfstrx _ _ _ _ _ _ H1). Qed.
imports: CoRN.algebra.CRings