proposition: Lemma BQprodDr x y z: ratp x -> ratp y -> ratp z -> x *q (y +q z) = (x *q y) +q (x *q z).
proof: Proof. move => xq yq zq. have H: forall x y, ratp x -> ratp y -> Q (x *q y) *z (P x *z P y) = P (x *q y) *z (Q x *z Q y). clear; move => x y xq yq; rewrite /BQprod /BQ_of_pair -lock /BQ_of_pair_internal. move /BQ_P: xq => [_ px /BZps_sBZ qx _]. move /BQ_P: yq => [_ py /BZps_sBZ qy _]. move:(BZgcd_div (ZSp px py) (ZSp qx qy)). move:(BZgcd_s2 (ZSp px py) (ZSp qx qy)). set a := (P x *z P y); set b:= (Q x *z Q y); set p := BZgcd a b. aw; move => [pZ u'Z v'Z] [e1 e2]; rewrite {2} e2 {1} e1. by rewrite BZprodC BZprodA // (BZprodC p). move: (QSs yq zq) (QSp xq yq) (QSp xq zq) => yzq xyq xzq. 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. move /BQ_P: xyq => [_ pxy qxyp _]; move:(BZps_sBZ qxyp) => qxy. move /BQ_P: xzq => [_ pxz qxzp _]; move:(BZps_sBZ qxzp) => qxz. set N := P x *z (P y *z Q z +z Q y *z P z). set D := Q x *z (Q y *z Q z). 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 N by apply:ZSp => //; apply:ZSs => //; apply:ZSp. have hd: inc D BZps by apply:(ZpsS_prod qxp (ZpsS_prod qyp qzp)). have he:intp (P (x *q y) *z Q (x *q z) +z Q (x *q y) *z P (x *q z)). by apply:ZSs; apply:ZSp. have hf: inc (Q (x *q y) *z Q (x *q z)) BZps by apply:ZpsS_prod. transitivity (BQ_of_pair N D). apply /(BQ_of_pair_prop5 ha hb hc hd). have ra: intp (Q y *z Q z) by apply: ZSp. have rb: intp (P y *z Q z +z Q y *z P z) by apply:ZSs; apply:ZSp. rewrite BZprodC /D - BZprodA // - (@BZprodA (Q x)) //; congr (_ *z _). rewrite BZprodC - BZprodA // (BZprodC _ N) /N - BZprodA //;congr (_ *z _). rewrite /BQsum /BQ_of_pair -lock /BQ_of_pair_internal pr1_pair pr2_pair. set N1 := (P y *z Q z +z Q y *z P z). move:(BZgcd_div rb ra)(BZgcd_s2 rb ra); move => [e1 e2][rc rd re]. set p := BZgcd N1 (Q y *z Q z);rewrite /N1 {2} e1 {1} e2. by rewrite BZprodA // (BZprodC (N1 %/z p)). apply /(BQ_of_pair_prop5 hc hd he hf). set Pxy := (P x *z P y); set Pxz := (P x *z P z). set Qxy := (Q x *z Q y); set Qxz := (Q x *z Q z). have ra: intp (P y *z Q z) by apply:ZSp. have rb: intp (Q y *z P z) by apply:ZSp. have rc: intp D by apply:BZps_sBZ. have rd: intp (P (x *q y) *z Q (x *q z)) by apply:ZSp. have re: intp (Q (x *q y) *z P (x *q z)) by apply:ZSp. have rf: intp (Q (x *q y) *z Q (x *q z)) by apply:ZSp. have rg: intp Pxy by apply:ZSp. have rh: intp Pxz by apply:ZSp. have ri: intp (Pxy *z Q z) by apply: ZSp. have rj: intp (Pxz *z Q y) by apply: ZSp. have rk: intp Qxy by apply: ZSp. have rl: intp (Q x *z Q z) by apply: ZSp. have -> : N = Pxy *z (Q z) +z Pxz *z (Q y). by rewrite /N BZprodDr// - BZprodA// - BZprodA// (BZprodC (Q y) (P z)). rewrite BZprodDr // BZprodC BZprodDr //; congr (_ +z _). rewrite (BZprodC (Q (x *q y))) - BZprodA // (@BZprodA D) // BZprodC. have ->: D = (Qxy *z Q z) by rewrite /D BZprodA. rewrite BZprodA // (BZprodC ((Qxy *z Q z))) BZprodA // H //. rewrite (BZprodC D) - (BZprodA) // - (BZprodA) //. have ->: D = (Q x *z Q z) *z Q y by rewrite /D (BZprodC (Q y)) - BZprodA //. by rewrite (BZprodA qxz rh qy) (H _ _ xq zq) - BZprodA //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)