proposition: Lemma sqrt2_prop : BRsqrt2 = BRsqrt \2r.
proof: Proof. move: BRsqrt2_prop => [/BRps_sBRp sa sb]. move:(BRsqrt_prop (BRps_sBRp RpsS2)) => [sc sd]. exact: (BRsqrt_unique (BRps_sBRp RpsS2) sa (esym sb) sd sc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)