proposition: Lemma BR_square_1 x: realp x -> (x *r x = \1r <-> (x = \1r \/ x = \1mr)).
proof: Proof. move => xr; split => eq; last first. case:eq => ->;first by rewrite (BRprod_1r RS1). by rewrite (BRprod_m1r RSm1) BRopp_m1. suff H: forall x, inc x BRps -> x *r x = \1r -> x = \1r. case/BR_i1P: xr => ha. + by left;move: eq; rewrite ha BRprod_0r. + by left; apply: H. + right; move:(BRms_sBR ha) => hb. move: (BRprod_opp_opp hb hb); rewrite eq => hc. move:(f_equal BRopp (H _ (BRopp_negative1 ha) hc)). by rewrite (BRopp_K hb) BRopp_1. move => y yp eq1; move:(BRps_sBR yp) => yr. move:(BR_inv_prop yr yr eq1) => h1. case: (rleT_ell (BRps_sBR yp) RS1) => // h2. move/(BQ_ltinv1 yp): (h2); rewrite - h1; move =>[h3 _]; BRo_tac. move:(h2); rewrite h1; move/(BQ_ltinv1 yp) => [h3 _]; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)