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