proposition: Lemma BQdiff_square a b: ratp a -> ratp b -> BQsquare (a -q b) = BQsquare a +q BQsquare b -q (BQdouble (a *q b)).
proof: Proof. move => aq bq. rewrite (BQsum_square aq (QSo bq)). rewrite {2}/BQsquare (BQprod_opp_opp bq bq). by rewrite /BQdouble - (BQopp_prod_r aq bq) - (BQopp_prod_r QS2 (QSp aq bq)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)