proposition: Lemma included3_interval : forall (I : interval) x y z Hxyz, I x -> I y -> I z -> included (compact (Min (Min x y) z) (Max (Max x y) z) Hxyz) I.
proof: Proof. intros I x y z Hxyz H H0 H1. apply included_interval'; auto. apply (included_interval I x y H H0 (Min_leEq_Max _ _)). apply compact_inc_lft. apply (included_interval I x y H H0 (Min_leEq_Max _ _)). apply compact_inc_rht. Qed.
imports: CoRN.ftc.NthDerivative