proposition: Lemma included_compact_in_interval2 : forall I pI x y Hx Hy, included (compact_in_interval2 I pI x y Hx Hy) I.
proof: Proof. induction I; simpl in |- *; intros; try inversion_clear Hx as (H,H0); try inversion_clear Hy as (H1,H2); red in |- *; simpl in |- *; intros x0 X; try inversion_clear X; auto. apply less_leEq_trans with (Min x y); try apply less_Min; auto. apply leEq_less_trans with (Max x y); try apply Max_less; auto. apply leEq_transitive with (Min x y); try apply leEq_Min; auto. apply leEq_transitive with (Max x y); try apply Max_leEq; auto. split. apply cip2' with (Min x y); try apply less_Min; auto. apply cip3' with (Max x y); try apply Max_less; auto. split. apply cip2' with (Min x y); try apply less_Min; auto. apply cip3 with (Max x y); try apply Max_leEq; auto. split. apply cip2 with (Min x y); try apply leEq_Min; auto. apply cip3' with (Max x y); try apply Max_less; auto. Qed.
imports: CoRN.ftc.NthDerivative