proposition: Lemma BRsquare_diff x y: realp x -> realp y -> BRsquare x -r BRsquare y = (x -r y) *r (x +r y).
proof: Proof. move => xr yr; move: (RSs xr yr) => sab. rewrite BRprodBl // !BRprodDr // (BRsumC (y *r x)) (BRprodC y x). by rewrite BRdiff_sum_simpl_r //; apply:RSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)