proposition: Lemma BRsqrt_prop x: inc x BRp -> x = BRsquare (BRsqrt x) /\ inc (BRsqrt x) BRp.
proof: Proof. move => h. apply:(select_pr (BRsqrt_exists h) (BRsqrt_unique h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)