proposition: Lemma compact_included : forall a b Hab (I : interval), I a -> I b -> included (compact a b Hab) I.
proof: Proof. induction I; red in |- *; simpl in |- *; intros X X0 x X1; try inversion_clear X; try inversion_clear X0; try inversion_clear X1. auto. apply less_leEq_trans with a; auto. apply leEq_less_trans with b; auto. apply leEq_transitive with a; auto. apply leEq_transitive with b; auto. split; [ apply less_leEq_trans with a | apply leEq_less_trans with b ]; auto. split; [ apply less_leEq_trans with a | apply leEq_transitive with b ]; auto. split; [ apply leEq_transitive with a | apply leEq_less_trans with b ]; auto. split; [ apply leEq_transitive with a | apply leEq_transitive with b ]; auto. Qed.
imports: CoRN.ftc.NthDerivative