proposition: Lemma Feq_transitive : Feq I F G -> Feq I G H -> Feq I F H.
proof: Proof. intro H0. elim H0; intros incF H'. elim H'; intros incG H1. clear H0 H'. intro H0. elim H0; intros incG' H'. elim H'; intros incH H2. clear H0 H'. FEQ. Step_final (G x (incG x X)). Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1