proposition: Lemma Continuous_I_nth : forall n : nat, Continuous_I Hab (F{^}n).
proof: Proof. simple induction n. apply Continuous_I_wd with ( [-C-]OneR). apply FNth_zero'; apply contin_imp_inc; auto. apply Continuous_I_const. clear n; intros. apply Continuous_I_wd with (F{*}F{^}n). apply FNth_mult'; apply contin_imp_inc; auto. apply Continuous_I_mult; assumption. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac