proposition: Lemma root_lt_x (n : nat) x y : (0 < n)%N -> 0 <= x -> 0 <= y -> (n.-root x < y) = (x < y ^+ n).
proof: Proof. by move=> Hn Hx Hy; rewrite -(ltr_pXn2r Hn) ?rootCK // nnegrE rootC_ge0. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)