proposition: Lemma BQinv_K x: ratp x -> BQinv (BQinv x) = x.
proof: Proof. move => xq; move/BQ_P: (xq) => [px nz /BZps_sBZ dz _]. case /BQ_i1P:xq => xs. + by rewrite xs BQinv_0 BQinv_0. + move: (QpsS_inv xs) => ixs. by rewrite (BQinv_pos ixs) (BQinv_pos xs); aw. + move: (QmsS_inv xs) => ixs. rewrite (BQinv_neg ixs) (BQinv_neg xs); aw. by rewrite (BZopp_K nz) (BZopp_K dz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)