proposition: Lemma Feq_nth : forall n : nat, Feq I F F' -> Feq I (F{^}n) (F'{^}n).
proof: Proof. intros n H0. elim H0; intros incF H0'. elim H0'; clear H0 H0'; intros incF' H1. FEQ. astepl (F x Hx[^]n); Step_final (Part F' x Hx'[^]n). Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1