proposition: Lemma nboundedC c : nbounded c%:S.
proof: Proof. apply/asboolP/nboundedP; exists (`|c| + 1). by rewrite ltr_pwDr. by move=> _; rewrite ltrDl. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.bigenough.bigenough mathcomp.classical(boolp classical_sets functions) mathcomp.classical(mathcomp_extra) xfinmap ereal reals discrete topology