proposition: Lemma BRsum_square a b: realp a -> realp b -> BRsquare (a +r b) = BRsquare a +r BRsquare b +r BRdouble (a *r b).
proof: Proof. move => ar br. move:(RSp ar ar)(RSp br br)(RSp ar br)(RSs ar br) => aar bbr abr sabr. rewrite {1}/BRsquare (BRprodDl sabr ar br). rewrite (BRprodDr ar ar br) (BRprodDr br ar br) (BRprodC b a). rewrite (BRsumC (a *r b)) (BRsum_ACA aar abr bbr abr). by rewrite BRdouble_s // BRdouble_C. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)