proposition: Lemma BQ_of_pair_prop3 a b c d (a' := a %/z (BZgcd a b)) (b' := b %/z (BZgcd a b)) (c' := c %/z (BZgcd c d)) (d' := d %/z (BZgcd c d)): intp a -> inc b BZps -> intp c -> inc d BZps -> (a *z d = b *z c <-> (a' = c' /\ b' = d')).
proof: Proof. move => az bzps cz dzps. move:(BZps_sBZ bzps) (BZps_sBZ dzps) => bz dz. move: (BQ_of_pair_prop1 az bzps) (BQ_of_pair_prop1 cz dzps). rewrite -/a' -/b' -/c' -/d'; move => [a'z b'zps cp1 be1] [c'z d'zps cp2 be2]. move:(BZgcd_div az bz) => [ {3} -> {3} -> ]. move:(BZgcd_div cz dz) => [ {3} -> {1} -> ]. have pabz:= (ZS_gcd az bz). have pcdz:= (ZS_gcd cz dz). have b'z := (BZps_sBZ b'zps). have d'z :=(BZps_sBZ d'zps). have ha := (ZSp pcdz d'z). have hb:=(ZSp pcdz c'z). have qa := (ZSp a'z d'z); have qb :=(ZSp b'z c'z). rewrite -(BZprodA pabz a'z ha) -(BZprodA pabz b'z hb) (BZprodC a') (BZprodC b'). rewrite -(BZprodA pcdz d'z a'z) -(BZprodA pcdz c'z b'z)(BZprodC d')(BZprodC c'). rewrite (BZprodA pabz pcdz qa) (BZprodA pabz pcdz qb). split; last by move => [-> ->]; rewrite (BZprodC d'). have ppz: intp (BZgcd a b *z BZgcd c d) by apply:ZSp. have ppnz: (BZgcd a b *z BZgcd c d) <> \0z. by apply: BZprod_nz => //; apply:BZgcd_nz1 => //; right; apply:BZps_nz. move/(BZprod_eq2l qa qb ppz ppnz). exact:BQ_of_pair_prop2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)