proposition: Fact sqrtr_subproof (x : R) : exists2 y, 0 <= y & (if 0 <= x then y ^+ 2 == x else y == 0) : bool.
proof: Proof. case x_ge0: (0 <= x); last by exists 0. have le0x1: 0 <= x + 1 by rewrite -nnegrE rpredD ?rpred1. have [|y /andP[y_ge0 _]] := @poly_ivt ('X^2 - x%:P) _ _ le0x1. rewrite !hornerE -subr_ge0 add0r expr0n sub0r opprK x_ge0 sqrrD mulr1. by rewrite addrAC !addrA addrK -nnegrE !rpredD ?rpredX ?rpred1. by rewrite rootE !hornerE subr_eq0; exists y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)