proposition: Lemma lub_charact : forall a b Hab F (contF : Continuous_I Hab F) z, fun_lub_IR F (compact a b Hab) z -> z [=] lub_funct a b Hab F contF.
proof: Proof. intros a b Hab F contF z H. elim H; intros Hz Hz'; clear H. assert (H := lub_is_lub _ _ _ _ contF). set (y := lub_funct _ _ _ _ contF) in *. elim H; intros Hy Hy'; clear H. apply leEq_imp_eq; apply shift_zero_leEq_minus'; apply inv_cancel_leEq; astepr ZeroR; apply approach_zero; intros e He. rstepl (z[-]y). apply shift_minus_less. elim (Hz' e He); intros x Hx. intro H. apply less_leEq_trans with (x[+]e). apply shift_less_plus'; auto. astepr (y[+]e). apply plus_resp_leEq; apply Hy. auto. rstepl (y[-]z). apply shift_minus_less. elim (Hy' e He); intros x Hx. intro H. apply less_leEq_trans with (x[+]e). apply shift_less_plus'; auto. astepr (z[+]e). apply plus_resp_leEq; apply Hz. auto. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac