proposition: Lemma BQsumdiff_square a b: ratp a -> ratp b -> BQsquare (a +q b) = \4q *q (a *q b) +q BQsquare (a -q b).
proof: Proof. move => aq bq. rewrite (BQdiff_square aq bq) (BQsum_square aq bq) - BQprod_22. have ha := (QSp aq bq). move: (BQdouble_p (QSdouble ha)); rewrite /BQdouble => hb. rewrite - (BQprodA QS2 QS2 ha) - hb. set u := (BQsquare a +q BQsquare b); set v := (BQdouble (a *q b)). have uq: inc u BQ by apply:QSs;apply:QSp. have vq: inc v BQ by apply:QSdouble; apply:QSp. rewrite (BQsum_ACA vq vq uq (QSo vq)) (BQsum_opp_r vq). rewrite BQsumC (BQsum_0r (QSs vq uq)). rewrite /v /BQdouble. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)