proposition: Lemma included_compact : forall (a b c d : IR) Hab Hcd, compact a b Hab c -> compact a b Hab d -> included (compact c d Hcd) (compact a b Hab).
proof: Proof. intros a b c d Hab Hcd H H0 x H1. inversion_clear H. inversion_clear H0. inversion_clear H1. split. apply leEq_transitive with c; auto. apply leEq_transitive with d; auto. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists