proposition: Lemma leEq_glb : forall a b Hab (F : PartIR) contF x, (forall y, Compact Hab y -> forall Hy, x [<=] F y Hy) -> x [<=] glb_funct a b Hab F contF.
proof: Proof. intros a b Hab F contF x H. elim (glb_is_glb _ _ _ _ contF); intros. astepr (glb_funct _ _ _ _ contF[+][0]); apply shift_leEq_plus'. apply approach_zero_weak. intros e H0. elim (b0 _ H0); intro y; intros. apply less_leEq; eapply leEq_less_trans. 2: apply q. apply minus_resp_leEq. elim p; intros z Hz. elim Hz; intros H1 H2. elim H2; intros H3 H4. astepr (F z H3); auto. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac