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