proposition: Lemma norm_fun_lub : forall e, [0] [<] e -> {x : IR | I x and (forall Hx, Norm_Funct[-]e [<] AbsIR (F x Hx))}.
proof: Proof. intros e H. cut {x : IR | I x and (forall Hx' : P x, Norm_Funct [<] AbsIR (F x Hx') [+]e)}. intro H0. elim H0; intros y Hy. elim Hy; clear H0 Hy; intros Hy Hy'. exists y; split. auto. intro; apply shift_minus_less; apply Hy'. generalize lub_is_lub. generalize glb_is_glb. intros H0 H1. cut {x : IR | I x and (forall Hx' : P x, F x Hx' [<] glb_funct[+]e [/]TwoNZ)}. cut {x : IR | I x and (forall Hx' : P x, lub_funct[-]e [/]TwoNZ [<] F x Hx')}. intros H2 H3. elim H2; intros x Hx. elim Hx; clear H2 Hx; intros Hx Hx0. elim H3; intros x' Hx'. elim Hx'; clear H3 Hx'; intros Hx' Hx'0. elim (less_cotransitive_unfolded _ _ _ (pos_div_two _ _ H) ( [--]glb_funct[-]lub_funct)); intro H2. exists x'; split. auto. unfold Norm_Funct in |- *. intro; eapply less_wdl. 2: apply eq_symmetric_unfolded; apply leEq_imp_Max_is_rht. apply shift_less_plus. rstepl ( [--] (glb_funct[+]e)). eapply less_leEq_trans. 2: apply inv_leEq_AbsIR. apply inv_resp_less. eapply less_transitive_unfolded. apply Hx'0 with (Hx' := Hx'1). apply plus_resp_less_lft. apply pos_div_two'; assumption. astepl ([0][+]lub_funct); apply less_leEq; apply shift_plus_less. assumption. exists x; split. auto. unfold Norm_Funct in |- *. intro; apply less_leEq_trans with (lub_funct[+]e [/]TwoNZ). apply Max_less. apply shift_less_plus'; astepl ZeroR. apply pos_div_two; assumption. apply shift_less_plus'; assumption. apply shift_leEq_plus. rstepl (lub_funct[-]e [/]TwoNZ). eapply leEq_transitive. apply less_leEq; apply Hx0 with (Hx' := Hx'1). apply leEq_AbsIR. elim H1; clear H1; intros H2 H3. elim (H3 _ (pos_div_two _ _ H)). intros x Hx; elim Hx; clear Hx; intros y Hx'; elim Hx'; clear Hx'; intros Hx' Hx''; elim Hx''; clear Hx''; intros Hx'' Hx'''. exists y; split. auto. intro; apply shift_minus_less; apply shift_less_plus'. eapply less_wdl; [ apply q | algebra ]. elim H0; clear H0; intros H2 H3. elim (H3 _ (pos_div_two _ _ H)). intros x Hx; elim Hx; clear Hx; intros y Hx'; elim Hx'; clear Hx'; intros Hx' Hx''; elim Hx''; clear Hx''; intros Hx'' Hx'''. exists y; split. auto. intro; apply shift_less_plus'. eapply less_wdl; [ apply q | algebra ]. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac