proposition: Lemma BRsqrt_unique x: inc x BRp -> singl_val2 (inc^~ BRp) (fun z => x = BRsquare z).
proof: Proof. move => xp u v /= ur up vr vp. have ha: BRsquare v <=r BRsquare v by rewrite - vp;apply:(rleR (BRp_sBR xp)). by rewrite up in vp; apply: rleA; apply:BRsquare_mon2 => //; rewrite vp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)