proposition: Lemma BQ_le_pair a b c d: intp a -> inc b BZps -> intp c -> inc d BZps -> ((BQ_of_pair a b) <=q (BQ_of_pair c d) <-> (a *z d) <=z (b *z c)).
proof: Proof. move => az bzps cz dzps. move: (BQ_of_pair_prop4 az bzps) (BQ_of_pair_prop4 cz dzps). set x := BQ_of_pair a b; set y := BQ_of_pair c d => xz yz. have h : x <=q y <-> BQle_aux x y by split => //; case. apply: (iff_trans h). rewrite /BQle_aux /x/y/BQ_of_pair - lock /BQ_of_pair_internal; aw. have bz:=(BZps_sBZ bzps). have bzp:=(BZps_sBZp bzps). have bnz:= (BZps_nz bzps). have hz: (a <> \0z \/ b <> \0z) by right. have dz:=(BZps_sBZ dzps). have dzp:=(BZps_sBZp dzps). have dnz:= (BZps_nz dzps). have hz': (c <> \0z \/ d <> \0z) by right. move: (BZgcd_div az bz)(BZgcd_div cz dz). set a' := a %/z BZgcd a b; set d':= d %/z BZgcd c d. set b' := b %/z BZgcd a b; set c':= c %/z BZgcd c d. move =>[av bv][cv dv]. move: (ZpS_gcd az bz) (ZpS_gcd cz dz) => gzp gz'p. move:(BZp_sBZ gzp) (BZp_sBZ gz'p) => gz gz'. have a'z:=(ZS_quo az gz). move:(BZ_positive_quo_gcd bzp az) (BZ_nz_quo_gcd bz az bnz). rewrite BZgcd_C => qp qnz. have b'zps: inc b' BZps by apply/BZps_iP. have c'z:=(ZS_quo cz gz'). move:(BZ_positive_quo_gcd dzp cz) (BZ_nz_quo_gcd dz cz dnz). rewrite BZgcd_C => qp' qnz'. have d'zps: inc d' BZps by apply/BZps_iP. rewrite av {2} bv dv {2} cv. move: (BZps_sBZ b'zps) (BZps_sBZ d'zps) => b'z d'z. rewrite (BZprod_ACA gz a'z gz' d'z) (BZprod_ACA gz b'z gz' c'z). apply: iff_sym. set w := (BZgcd a b *z BZgcd c d). have wp: inc w BZps. by apply:ZpsS_prod; apply/BZps_iP; split => //;apply: BZgcd_nz1. rewrite (BZprodC w) (BZprodC w). apply: (BZprod_ple2r (ZSp a'z d'z) (ZSp b'z c'z) wp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)