proposition: Lemma BQinv_sign x: ratp x -> BQsign (BQinv x) = BQsign x.
proof: Proof. case/BQ_i1P => xs. + by rewrite xs BQinv_0. + by rewrite (BQsign_pos (QpsS_inv xs)) (BQsign_pos xs). + by rewrite (BQsign_neg (QmsS_inv xs)) (BQsign_neg xs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)