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