proposition: Lemma bigcup_ballT {R : realType} : \bigcup_n ball (0%R : R) n%:R = setT.
proof: Proof. apply/seteqP; split => // x _; have [x0|x0] := ltP 0%R x. exists `|ceil x|.+1 => //. rewrite /ball /= sub0r normrN gtr0_norm// (le_lt_trans (ceil_ge _))//. by rewrite -natr1 natr_absz -abszE gtz0_abs// ?ceil_gt0// ltr_pwDr. exists `|ceil (- x)|.+1 => //. rewrite /ball /= sub0r normrN ler0_norm// (le_lt_trans (ceil_ge _))//. rewrite -natr1 natr_absz -abszE gez0_abs ?ceil_ge0// 1?lerNr ?oppr0//. by rewrite ltr_pwDr. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule