proposition: Lemma BQ_square_Z x y: ratp x -> BQsquare x = BQ_of_Z y -> [/\ inc y BZp, Qnum x *z Qnum x = y & Qden x = \1z].
proof: Proof. move => xq; rewrite (BQ_squarep xq) => sqx. move /BQ_P: xq => [_ nz dzp _]; move:(BZps_sBZ dzp) => dz. have pe: inc (P x *z P x) BZp. case /BZ_i0P: nz => ha; first exact:(BZps_sBZp (ZmsuS_prod ha ha)). exact:(ZpS_prod ha ha). move:(pr1_def sqx) => sa;split => //; first by ue. move:(pr2_def sqx) => /(BZprod_1_inversion_l dz dz) [_] [] // xn. rewrite xn in dzp; case: (BZ_di_neg_spos ZmsS_m1 dzp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)