proposition: Lemma ubound_subproof (x : creal) : {b : F | b > 0 & forall i, `|x i| <= b}.
proof: Proof. pose_big_enough i; first set b := 1 + `|x i|. exists (foldl maxr b [seq `|x n| | n <- iota 0 i]) => [|n]. have : 0 < b by rewrite ltr_spaddl. by elim: iota b => //= a l IHl b b_gt0; rewrite IHl ?lt_maxr ?b_gt0. have [|le_in] := (ltnP n i). elim: i b => [|i IHi] b //. rewrite ltnS -addn1 iotaD add0n map_cat foldl_cat /= le_maxr leq_eqVlt. by case/orP=> [/eqP->|/IHi->] //; rewrite lexx orbT. set xn := `|x n|; suff : xn <= b. by elim: iota xn b => //= a l IHl xn b Hxb; rewrite IHl ?le_maxr ?Hxb. rewrite -ler_subl_addr (le_trans (ler_norm _)) //. by rewrite (le_trans (ler_dist_dist _ _)) ?ltW ?cauchymodP. by close. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)