proposition: Lemma included_Feq' : forall (I : interval) F G, (forall a b Hab, included (compact a b Hab) I -> Feq (Compact Hab) F G) -> Feq I F G.
proof: Proof. intros I F G H. apply eq_imp_Feq. intros x H0. elim (H x x (leEq_reflexive _ x) (compact_single_iprop I x H0)); intros. apply a; apply compact_single_prop. intros x H0. elim (H x x (leEq_reflexive _ x) (compact_single_iprop I x H0)); intros. inversion_clear b. apply X; apply compact_single_prop. intros x H0 Hx Hx'. elim (H x x (leEq_reflexive _ x) (compact_single_iprop I x H0)); intros. inversion_clear b. apply H1; apply compact_single_prop. Qed.
imports: CoRN.ftc.NthDerivative