proposition: Lemma PartInt_strext : forall x y Hx Hy, f (Build_subcsetoid_crr IR _ x Hx) [#] f (Build_subcsetoid_crr IR _ y Hy) -> x [#] y.
proof: Proof. intros x y Hx Hy H. exact (csf_strext_unfolded _ _ _ _ _ H). Qed.
imports: CoRN.ftc.IntervalFunct