proposition: Lemma BRsquare_inj x y: realp x -> realp y -> (BRsquare x = BRsquare y <-> (x = y \/ x = BRopp y)).
proof: Proof. move => xr yr. move:(RSp yr yr)(RSs xr yr)(RS_diff xr yr) => sa sb sc. split. move => h. have: BRsquare x -r BRsquare y = \0r by rewrite h (BRdiff_xx sa). rewrite (BRsquare_diff xr yr); move /(BRprod_nz_bis sc sb); case. by move/(BRdiff_xx_rw xr yr) ; left. by rewrite -{1} (BRopp_K yr); move/(BRdiff_xx_rw xr (RSo yr)); right. by case => -> //; rewrite /BRsquare; apply: BRprod_opp_opp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)