proposition: Lemma included2_compact : forall x y Hxy, Compact Hab x -> Compact Hab y -> included (compact (Min x y) (Max x y) Hxy) (Compact Hab).
proof: Proof. do 3 intro. intros H H0. inversion_clear H. inversion_clear H0. apply included_compact; split. apply leEq_Min; auto. apply leEq_transitive with y. apply Min_leEq_rht. auto. apply leEq_transitive with y. auto. apply rht_leEq_Max. apply Max_leEq; auto. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists