proposition: Lemma BQ_square_1 x: ratp x -> (BQsquare x = \1q <-> (x = \1q \/ x = \1mq) ).
proof: Proof. move => xq; split. move /BQ_P:(xq) => [pa nz _ _ ]. move /(BQ_square_Z xq) => [_ /(BZprod_1_inversion_l nz nz) [_ sa] sb]. by case: sa => sa; [left | right]; rewrite - pa sa sb. case => ->; rewrite /BQsquare. by rewrite (BQprod_1l QS1). by rewrite (BQprod_m1l QSm1) BQopp_m1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)