proposition: Lemma BQ_squarep x: ratp x -> BQsquare x = J (Qnum x *z Qnum x) (Qden x *z Qden x).
proof: Proof. move => xq; move /BQ_P:(xq) => [_ nz dzp cp]; move: (BZps_sBZ dzp)=> dz. rewrite /BQsquare /BQprod /BQ_of_pair -lock /BQ_of_pair_internal. set p := BZgcd (P x *z P x) (Q x *z Q x). suff: p = \1z by move ->; rewrite ! BZquo_one //; apply:ZSp. have ha: BZcoprime (Q x) (P x) by rewrite /BZcoprime BZgcd_C. have hb: BZcoprime (P x *z P x) (Q x). by rewrite /BZcoprime BZgcd_C BZgcd_simp. by rewrite /p BZgcd_simp //; apply:ZSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)