proposition: Lemma leEq_Norm_Funct : forall e, (forall x, I x -> forall Hx, AbsIR (F x Hx) [<=] e) -> Norm_Funct [<=] e.
proof: Proof. intros e H. astepr ([0][+]e); apply shift_leEq_plus. apply approach_zero_weak. intros d Hd. apply shift_minus_leEq. elim (norm_fun_lub d Hd); intros x Hx. elim Hx; clear Hx; intros Hx Hx'. apply plus_cancel_leEq_rht with ( [--] (AbsIR (F x (Hinc' x Hx)))). astepl (Norm_Funct[-]AbsIR (F x (Hinc' x Hx))). apply less_leEq; apply less_leEq_trans with d. apply shift_minus_less; apply shift_less_plus'; apply Hx'. rstepr (d[+] (e[-]AbsIR (F x (Hinc' x Hx)))). astepl (d[+][0]); apply plus_resp_leEq_lft. apply shift_leEq_minus; astepl (AbsIR (F x (Hinc' x Hx))); apply H; assumption. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac