proposition: Lemma glb_prop : forall x : IR, I x -> forall Hx, glb_funct [<=] F x Hx.
proof: Proof. intros. elim glb_is_glb. intros. apply a0. exists x. split; algebra. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac