proposition: Lemma QS_inv x: ratp x -> ratp (BQinv x).
proof: Proof. case /BQ_i1P => xs. + rewrite xs BQinv_0; apply: QS0. + by move: (QpsS_inv xs) => /BQps_sBQ. + by move: (QmsS_inv xs) => /BQms_sBQ. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)