proposition: Lemma BQprod_abs x y: ratp x -> ratp y -> BQabs (x *q y) = (BQabs x) *q (BQabs y).
proof: Proof. move => xq yq. case /BQ_i0P: (xq)=> pa; case /BQ_i0P: (yq)=> pb. + rewrite (BQabs_negs pa) (BQabs_negs pb) (BQprod_opp_opp xq yq). by rewrite (BQabs_pos (BQps_sBQp (QmsuS_prod pa pb))). + rewrite (BQabs_negs pa) (BQabs_pos pb) - ( BQopp_prod_l xq yq). by rewrite BQprodC (BQabs_neg (QpmS_prod pb (BQms_sBQm pa))). + rewrite (BQabs_negs pb) (BQabs_pos pa) - ( BQopp_prod_r xq yq). by rewrite (BQabs_neg (QpmS_prod pa (BQms_sBQm pb))). + by rewrite (BQabs_pos pa) (BQabs_pos pb) (BQabs_pos (QpS_prod pa pb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)