proposition: Lemma BQprodA x y z: ratp x -> ratp y -> ratp z -> x *q (y *q z) = (x *q y) *q z.
proof: Proof. suff H:forall x y z, ratp x -> ratp y -> ratp z -> x *q (y *q z) = BQ_of_pair (Qnum x *z Qnum y *z Qnum z) (Qden x *z Qden y *z Qden z). move => xQ yQ zQ; rewrite (BQprodC (x *q y) z) H // H //. move /BQ_P: xQ => [_ px /BZps_sBZ qx _]. move /BQ_P: yQ => [_ py /BZps_sBZ qy _]. move /BQ_P: zQ => [_ pz /BZps_sBZ qz _]. apply: f_equal2. by rewrite (BZprodC (P x)) - BZprodA // (BZprodC (P x)) (BZprodC (P y)). by rewrite (BZprodC (Q x)) - BZprodA // (BZprodC (Q x)) (BZprodC (Q y)). clear; move => x y z xQ yQ zQ; move:(QSp yQ zQ) => yzQ. move /BQ_P: xQ => [_ px qxp _]; move:(BZps_sBZ qxp) => qx. move /BQ_P: yQ => [_ py qyp _]; move:(BZps_sBZ qyp) => qy. move /BQ_P: zQ => [_ pz qzp _]; move:(BZps_sBZ qzp) => qz. move /BQ_P: yzQ => [_ pyz qyzp _]; move:(BZps_sBZ qyzp) => qyz. have ha: intp (P x *z P (y *q z)) by apply:ZSp. have hb: inc (Q x *z Q (y *q z)) BZps by apply: ZpsS_prod. have hc: intp ((P x *z P y) *z P z) by apply:ZSp => //; apply:ZSp. have hd:= (ZpsS_prod (ZpsS_prod qxp qyp) qzp). apply /(BQ_of_pair_prop5 ha hb hc hd). rewrite - (BZprodA qx qy qz) - (BZprodA px py pz). set u := (P y *z P z); set v := (Q y *z Q z). have uz: intp u by apply:ZSp. have vz: intp v by apply:ZSp. have he: intp (Q x *z v) by apply:ZSp. have hf: intp (P x *z u) by apply:ZSp. have hi: intp (P (y *q z) *z v) by apply:ZSp. have hj: intp (Q (y *q z) *z u) by apply:ZSp. rewrite - BZprodA // - BZprodA // (BZprodC (Q x)) (BZprodA pyz vz qx). rewrite (BZprodC (P x) u) (BZprodA qyz uz px) (BZprodC _ (Q x)) BZprodA //. rewrite (BZprodC _ (P x)) (BZprodA qx px hj) (BZprodC (P x)). apply: f_equal. rewrite /BQprod /BQ_of_pair -lock /BQ_of_pair_internal pr1_pair pr2_pair -/u -/v. move: (BZgcd_div uz vz); set p := BZgcd u v; move => [e1 e2]. rewrite {2} e1 {1} e2 (BZprodC p) (BZprodC p). move:(BZgcd_s2 uz vz) => [pZ u'Z v'Z]. rewrite BZprodA // BZprodA // (BZprodC (u %/z p)) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)