proposition: Lemma included_Feq : forall P Q F G, included P Q -> Feq Q F G -> Feq P F G.
proof: Proof. intros P Q F G H H0. elim H0; clear H0; intros H0 H1. elim H1; clear H1; intros H1 H2. apply eq_imp_Feq. eapply included_trans. apply H. assumption. eapply included_trans. apply H. assumption. intros; apply H2. apply H; assumption. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1