proposition: Lemma BRsumdiff_square a b: realp a -> realp b -> BRsquare (a +r b) = \4r *r (a *r b) +r BRsquare (a -r b).
proof: Proof. move => ar br. rewrite (BRdiff_square ar br) (BRsum_square ar br) - BRprod_22. have ha := (RSp ar br). move: (BRdouble_s (RSdouble ha)); rewrite - BRdouble_C /BRdouble => hb. rewrite - (BRprodA RS2 RS2 ha) - hb. set u := (BRsquare a +r BRsquare b); set v := (BRdouble (a *r b)). have ur: realp u by apply:RSs; apply:RSp. have vr: realp v by apply:RSdouble;apply:RSp. rewrite (BRsum_ACA vr vr ur (RSo vr)) (BRsum_opp_r vr). by rewrite BRsumC (BRsum_0r (RSs vr ur)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)