proposition: Lemma less_Norm_Funct : forall e, (forall x, I x -> forall Hx, AbsIR (F x Hx) [<] e) -> Norm_Funct [<=] e.
proof: Proof. intros x H. apply leEq_Norm_Funct. intros; apply less_leEq; apply H; assumption. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac