proposition: Lemma included_imp_norm_leEq : forall a b c d Hab Hcd F contF1 contF2, included (compact c d Hcd) (compact a b Hab) -> Norm_Funct (Hab:=Hcd) (F:=F) contF2 [<=] Norm_Funct (Hab:=Hab) (F:=F) contF1.
proof: Proof. intros. apply leEq_Norm_Funct; intros. apply norm_bnd_AbsIR; auto. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac