proposition: Lemma BQsum_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. move:(QSp aq aq)(QSp bq bq)(QSp aq bq)(QSs aq bq) => aaq bbq abq sabq. rewrite {1}/BQsquare (BQprodDl sabq aq bq). rewrite (BQprodDr aq aq bq) (BQprodDr bq aq bq) (BQprodC b a). rewrite (BQsumC (a *q b)) (BQsum_ACA aaq abq bbq abq). by rewrite (BQdouble_p abq) BQprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)