proposition: Lemma BRdiff_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. rewrite (BRsum_square ar (RSo br)). rewrite {2}/BRsquare (BRprod_opp_opp br br). by rewrite /BRdouble - (BRopp_prod_r ar br) - (BRopp_prod_r RS2 (RSp ar br)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)