proposition: Lemma IRecip_strext : forall x y : subset I, ([1][/] g x[//]Hg x) [#] ([1][/] g y[//]Hg y) -> x [#] y.
proof: Proof. intros x y H. elim (div_strext _ _ _ _ _ _ _ H); intro H0. elim (ap_irreflexive_unfolded _ _ H0). exact (csf_strext_unfolded _ _ _ _ _ H0). Qed.
imports: CoRN.ftc.PartFunEquality