proposition: Lemma BQabs_sign x: ratp x -> x = (BQQsign x) *q (BQabs x).
proof: Proof. move => xq; case /BQ_i1P: (xq) => xs. + rewrite xs BQabs_0 BQprod_0r //; apply:QS_qsign. + by rewrite (BQabs_pos (BQps_sBQp xs)) /BQQsign (BQsign_pos xs) BQprod_1l. + rewrite (BQabs_negs xs) /BQQsign (BQsign_neg xs) (BQprod_m1l (QSo xq)). by rewrite (BQopp_K xq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)