proposition: Lemma norm_bnd_AbsIR : forall x, I x -> forall Hx, AbsIR (F x Hx) [<=] Norm_Funct.
proof: Proof. intros. generalize lub_is_lub. generalize glb_is_glb. intros; simpl in |- *; unfold ABSIR in |- *. apply Max_leEq. apply leEq_transitive with lub_funct. apply lub_prop; auto. unfold Norm_Funct in |- *; apply lft_leEq_Max. apply leEq_transitive with ( [--]glb_funct). apply inv_resp_leEq. apply glb_prop; auto. unfold Norm_Funct in |- *; apply rht_leEq_Max. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac