proposition: Lemma included_imp_inc : forall (J : interval) P, (forall a b Hab, included (compact a b Hab) J -> included (compact a b Hab) P) -> included J P.
proof: Proof. intros J P H x H0. apply (H _ _ (leEq_reflexive _ _) (compact_single_iprop J x H0)). apply compact_inc_lft. Qed.
imports: CoRN.ftc.NthDerivative