fact: Definition upper_nthrootP (x : R) i : (bound x <= i)%N -> x < 2%:R ^+ i := @ssrnum.Num.Theory.mc_2_0.upper_nthrootP R x i.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)