proposition: Lemma included_interval' : forall (I : interval) x y z w, I x -> I y -> I z -> I w -> forall H, included (compact (Min x z) (Max y w) H) I.
proof: Proof. intros I x y z w; induction I; simpl in |- *; intros X X0 X1 X2 H; red in |- *; intros t Ht; inversion_clear Ht; simpl in |- *; try inversion_clear X; try inversion_clear X0; try inversion_clear X1; try inversion_clear X2; try split. apply less_leEq_trans with (Min x z); try apply less_Min; auto. apply leEq_less_trans with (Max y w); try apply Max_less; auto. apply leEq_transitive with (Min x z); try apply leEq_Min; auto. apply leEq_transitive with (Max y w); try apply Max_leEq; auto. apply less_leEq_trans with (Min x z); try apply less_Min; auto. apply leEq_less_trans with (Max y w); try apply Max_less; auto. apply less_leEq_trans with (Min x z); try apply less_Min; auto. apply leEq_transitive with (Max y w); try apply Max_leEq; auto. apply leEq_transitive with (Min x z); try apply leEq_Min; auto. apply leEq_less_trans with (Max y w); try apply Max_less; auto. apply leEq_transitive with (Min x z); try apply leEq_Min; auto. apply leEq_transitive with (Max y w); try apply Max_leEq; auto. Qed.
imports: CoRN.ftc.NthDerivative