proposition: Lemma lt_ubound (x : creal F) : (x < (ubound x + 1)%:CR)%CR.
proof: Proof. pose_big_enough i. apply: (@lt_crealP _ 1 i i) => //=; rewrite lerD2r. apply: le_trans (uboundP x i); exact: ler_norm. by close. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)