proposition: Lemma QpsS_inv x: inc x BQps -> inc (BQinv x) BQps.
proof: Proof. move => xp; rewrite (BQinv_pos xp). move/Zo_P: xp => [/BQ_P [_ nz dzp cp] nzp];move:(BZps_sBZ dzp)=> dz. suff: (BQ_of_pair (Q x) (P x)) = (J (Q x) (P x)). by move <-; apply: BQ_of_pair_spos. by rewrite /BQ_of_pair -lock /BQ_of_pair_internal BZgcd_C cp ! BZquo_one. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)