proposition: Lemma interval_convex: forall (a b : IR) (I : interval), I a -> I b -> included (clcr a b) I.
proof: Proof. intros ? ? ? Ha Hb. unfold included. intros x Hab. simpl in Hab. destruct Hab as [Hab Habr]. destruct I; simpl in Ha, Hb; simpl; try (split; destruct Ha, Hb); eauto using leEq_less_trans, leEq_reflexive, less_leEq_trans, leEq_transitive. Qed.
imports: CoRN.ftc.NthDerivative