proposition: Lemma BQprod_1l x: ratp x -> \1q *q x = x.
proof: Proof. move => xq; rewrite /BQprod /BQ_of_pair /BQ_one /BQ_of_Z; aw. move /BQ_P: (xq) => [_ pa /BZps_sBZ pb _]. by rewrite BZprod_1l // BZprod_1l //; apply: BQ_pr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)