proposition: Lemma BQinv_abs x: ratp x -> BQabs (BQinv x) = BQinv (BQabs x).
proof: Proof. move => xq. case/BQ_i1P: (xq) => h. + by rewrite h BQabs_0 BQinv_0 BQabs_0. + by rewrite (BQabs_pos (BQps_sBQp(QpsS_inv h))) (BQabs_pos (BQps_sBQp h)). + by rewrite (BQabs_negs (QmsS_inv h)) (BQabs_negs h) (BQinv_opp xq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)