proposition: Lemma compact_compact_in_interval2 : forall I pI x y Hx Hy, compact_ (compact_in_interval2 I pI x y Hx Hy).
proof: Proof. intro. elim I; simpl in |- *; intros; try inversion_clear Hx; try inversion_clear Hy; try apply ts; apply less_leEq. apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ]. apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ]. apply shift_minus_less; apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ]. apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ]. apply shift_minus_less; apply leEq_less_trans with (Max x y); [ apply Min_leEq_Max | apply less_plusOne ]. eapply less_transitive_unfolded; [ apply cip1'' | eapply leEq_less_trans; [ apply Min_leEq_Max | apply cip1'''' ] ]; try apply less_Min; try apply Max_less; auto. eapply less_leEq_trans; [ apply cip1'' | eapply leEq_transitive; [ apply Min_leEq_Max | apply cip1''' ] ]; try apply less_Min; try apply Max_leEq; auto. eapply leEq_less_trans; [ apply cip1' | eapply leEq_less_trans; [ apply Min_leEq_Max | apply cip1'''' ] ]; try apply leEq_Min; try apply Max_less; auto. auto. Qed.
imports: CoRN.ftc.NthDerivative