proposition: Lemma nth_root x n : x > 0 -> { y | y > 0 & y ^+ (n.+1) = x }.
proof: Proof. move=> l0x. case: (ltrgtP x 1)=> hx; last by exists 1; rewrite ?hx ?lter01// expr1n. case: (@poly_ivt ('X ^+ n.+1 - x%:P) 0 1); first by rewrite ler01. rewrite in_itv /= ?(hornerE, horner_exp) expr0n expr1n. by rewrite sub0r oppr_le0 subr_ge0 !ltW. move=> y hy; rewrite rootE ?(hornerE, horner_exp) subr_eq0. move/eqP=> hyx; exists y; rewrite //= lt0r (itvP hy) andbT. by apply: contra_eq_neq hyx => ->; rewrite expr0n /=; case: sgrP l0x. case: (@poly_ivt ('X ^+ n.+1 - x%:P) 0 x); first by rewrite ltW. rewrite in_itv /= ?(hornerE, horner_exp) expr0n sub0r oppr_le0 subr_ge0. by rewrite ler_eexpr // ltW. move=> y hy; rewrite rootE ?(hornerE, horner_exp) subr_eq0. move/eqP=> hyx; exists y; rewrite //= lt0r (itvP hy) andbT. by apply: contra_eq_neq hyx => ->; rewrite expr0n /=; case: sgrP l0x. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp) mathcomp(polyorder path interval ssrint)