proposition: Lemma interval_Min: forall {a b : IR} {I : interval}, I a -> I b -> I (Min a b).
proof: Proof. intros ? ? ? Ha Hb. destruct I; simpl in Ha, Hb; simpl; try (split; destruct Ha, Hb); eauto using leEq_less_trans, leEq_reflexive, leEq_transitive, Min_leEq_lft, less_Min, leEq_Min. Qed.
imports: CoRN.ftc.NthDerivative