proposition: Lemma included_Feq'' : forall I F G, proper I -> (forall a b Hab (Hab':=(less_leEq _ a b Hab)), included (Compact Hab') I -> Feq (Compact Hab') F G) -> Feq I F G.
proof: Proof. intros I F G H H0. apply eq_imp_Feq. intros x H1. elim (compact_proper_in_interval I x x (leEq_reflexive _ x)); Included. 2: exact (compact_single_iprop I x H1). intros a Ha. elim Ha; clear Ha. intros b Hb. elim Hb; clear Hb. intros Hab H2 H3. elim (H0 _ _ _ H2); intros. apply a0; apply H3; apply compact_single_prop. intros x H1. elim (compact_proper_in_interval I x x (leEq_reflexive _ x)); Included. 2: exact (compact_single_iprop I x H1). intros a Ha. elim Ha; clear Ha. intros b Hb. elim Hb; clear Hb. intros Hab H2 H3. elim (H0 _ _ _ H2); intros. inversion_clear b0. apply X; apply H3; apply compact_single_prop. intros x H1 Hx Hx'. elim (compact_proper_in_interval I x x (leEq_reflexive _ x)); Included. 2: exact (compact_single_iprop I x H1). intros a Ha. elim Ha; clear Ha. intros b Hb. elim Hb; clear Hb. intros Hab H2 H3. elim (H0 _ _ _ H2); intros. inversion_clear b0. apply H4; apply H3; apply compact_single_prop. Qed.
imports: CoRN.ftc.NthDerivative