proposition: Lemma BQsumA 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 Qden y *z Qden z +z Qnum y *z Qden x *z Qden z +z Qnum z *z Qden y *z Qden x) (Qden x *z Qden y *z Qden z). move => xq yq zq; rewrite (BQsumC (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. have ha: inc ((P z *z Q y) *z Q x) BZ by apply:ZSp => //; apply:ZSp. have hb: inc ((P x *z Q y) *z Q z) BZ by apply:ZSp => //; apply:ZSp. have hc: inc ((P y *z Q x) *z Q z) BZ by apply:ZSp => //; apply:ZSp. rewrite BZsumC (BZsumA ha hb hc). rewrite - (BZprodA pz qy qx) (BZprodC (Q y)) (BZprodA pz qx qy). by rewrite - (BZprodA px qy qz) (BZprodC (Q y)) (BZprodA px qz qy). by rewrite (BZprodC (Q x)) - BZprodA // (BZprodC (Q x)) (BZprodC (Q y)). clear. move => x y z xq yq zq; move:(QSs yq zq) => yzq. move /BQ_P: xq => [_ nx dxp _]; move:(BZps_sBZ dxp) => dx. move /BQ_P: yq => [_ ny dyp _]; move:(BZps_sBZ dyp) => dy. move /BQ_P: zq => [_ nz dzp _]; move:(BZps_sBZ dzp) => dz. move /BQ_P: yzq => [_ nyz dyzp _]; move:(BZps_sBZ dyzp) => dyz. have ha: intp(P x *z Q (y +q z) +z Q x *z P (y +q z)) by apply:ZSs; apply:ZSp. have hb:= (ZpsS_prod dxp dyzp). have hc: intp (((P x *z Q y) *z Q z +z (P y *z Q x) *z Q z) +z (P z *z Q y) *z Q x). by apply:ZSs; try apply:ZSs; apply:ZSp => //; apply:ZSp. have hd:= (ZpsS_prod (ZpsS_prod dxp dyp) dzp). apply /(BQ_of_pair_prop5 ha hb hc hd). set A := (P x *z Q (y +q z) +z Q x *z P (y +q z)). set B := (((P x *z Q y) *z Q z +z (P y *z Q x) *z Q z) +z (P z *z Q y) *z Q x). have he: intp (Q x *z Q y) by apply:ZSp. have hf: intp (Q z *z A) by apply:ZSp. have hg: intp (P y *z Q z) by apply:ZSp. have hi: intp (P z *z Q y) by apply:ZSp. have hj: intp (Q y *z P z) by apply:ZSp. set u :=(P y *z Q z +z Q y *z P z) ; set v := (Q y *z Q z). have uz: intp u by apply:ZSs. have vzps:= (ZpsS_prod dyp dzp). have vz := (BZps_sBZ vzps). rewrite BZprodC - BZprodA // - BZprodA // - BZprodA //; congr (_ *z _). have ->: B = P x *z v +z Q x *z u. move: (ZSp (ZSp nx dy) dz) (ZSp (ZSp ny dx) dz) (ZSp hi dx) => sa sb sc. rewrite /B - BZsumA // BZprodA//; apply: f_equal. rewrite (BZprodC _ (Q x)) (BZprodC _ (Q x)) - BZprodA // BZprodDr //. by rewrite (BZprodC (Q y)). rewrite BZprodA // /A /BQsum /BQ_of_pair -lock /BQ_of_pair_internal. rewrite pr1_pair pr2_pair. move: (BZgcd_s2 uz vz) (BZgcd_div uz vz) . set p := BZgcd u v; set u' := (u %/z p); set v' := (v %/z p). move => [pZ u'Z v'Z]. have ka : intp (v' *z P x) by apply:ZSp. have kb : intp (u' *z Q x) by apply:ZSp. rewrite -/v; move => [-> ->]. rewrite (BZprodC (P x) (p *z v')) - (BZprodA pZ v'Z nx) (BZprodC (P x) v'). rewrite (BZprodC (Q x) (p *z u')) - (BZprodA pZ u'Z dx) (BZprodC (Q x) u'). by rewrite - BZprodDr // (BZprodC p) BZprodA //; apply:ZSs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)