proposition: Lemma BQ_self_inv x: ratp x -> (x = BQinv x <-> [\/ x= \0q, x = \1q | x = \1mq]).
proof: Proof. move => xq; split. move => h; case: (equal_or_not x \0q) => e0; first by constructor 1. move: (f_equal (fun z => x *q z) h). rewrite (BQprod_inv1 xq e0) => /(BQ_square_1 xq). by case => hh;[constructor 2 | constructor 3]. by case => ->; [rewrite BQinv_0 | rewrite BQinv_1 | rewrite BQinv_m1 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)