proposition: Lemma compact_proper_in_interval : forall (J : interval) a b Hab, included (compact a b Hab) J -> proper J -> {a' : IR | {b' : IR | {Hab' : _ | included (compact a' b' (less_leEq _ _ _ Hab')) J | included (Compact Hab) (Compact (less_leEq _ _ _ Hab'))}}}.
proof: Proof. intros J a b Hab H H0. exists (Lend (compact_compact_in_interval2 J H0 a b (H _ (compact_inc_lft _ _ Hab)) (H _ (compact_inc_rht _ _ Hab)))). exists (Rend (compact_compact_in_interval2 J H0 a b (H _ (compact_inc_lft _ _ Hab)) (H _ (compact_inc_rht _ _ Hab)))). exists (proper_compact_in_interval2' _ _ _ _ _ _ (compact_compact_in_interval2 J H0 a b (H _ (compact_inc_lft _ _ Hab)) (H _ (compact_inc_rht _ _ Hab)))). eapply included_trans. apply compact_interval_inc. apply included_compact_in_interval2. apply included_compact. apply iprop_compact_in_interval2x'. apply iprop_compact_in_interval2y'. Qed.
imports: CoRN.ftc.NthDerivative