proposition: Lemma Norm_Funct_wd : forall a b Hab F G, Feq (compact a b Hab) F G -> forall contF contG, Norm_Funct (Hab:=Hab) (F:=F) contF [=] Norm_Funct (Hab:=Hab) (F:=G) contG.
proof: Proof. intros a b Hab F G H contF contG. elim H; intros incF H''. elim H''; clear H''; intros incG H''. unfold Norm_Funct in |- *; apply bin_op_wd_unfolded. generalize (lub_is_lub _ _ _ _ contF); intro Hlub. apply lub_charact. elim Hlub; clear Hlub; intros H0 H1. split. intros x H2. apply H0. apply fun_image_wd with G. apply Feq_symmetric; auto. auto. intros e H2. elim (H1 e H2); intro x; intros. exists x. apply fun_image_wd with F; auto. auto. apply un_op_wd_unfolded. generalize (glb_is_glb _ _ _ _ contF); intro Hglb. apply glb_charact. elim Hglb; intros H0 H1. split. intros x H2. apply H0. apply fun_image_wd with G. apply Feq_symmetric; auto. auto. intros e H2. elim (H1 e H2); intro x; intros. exists x. apply fun_image_wd with F; auto. auto. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac