proposition: Lemma eq_imp_Feq : included I P -> included I Q -> (forall x, I x -> forall Hx Hx', F x Hx [=] G x Hx') -> Feq I F G.
proof: Proof. intros. split. assumption. split; assumption. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1