proposition: Lemma le_ubound (x : creal F) : (x <= (ubound x)%:CR)%CR.
proof: Proof. apply: (@le_crealP _ 0%N) => j _ /=. apply: le_trans (uboundP x j); exact: ler_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals)