proposition: Lemma part_function_recip_strext : forall x y Hx Hy, ([1][/] _[//]Ext2R x Hx) [#] ([1][/] _[//]Ext2R y Hy) -> x [#] y.
proof: Proof. intros x y Hx Hy H. elim (div_strext _ _ _ _ _ _ _ H); intro H1. exfalso; apply ap_irreflexive_unfolded with (x := [1]:X); auto. exact (pfstrx _ _ _ _ _ _ H1). Qed.
imports: CoRN.algebra.CRings