proposition: Lemma Continuous_I_imp_abs_lub : {z : IR | forall x, I x -> forall Hx, AbsIR (F x Hx) [<=] z}.
proof: Proof. exists Norm_Funct. exact norm_bnd_AbsIR. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac