proposition: Lemma qleA x y: x <=q y -> y <=q x -> x = y.
proof: Proof. move => [/BQ_P [px nxz dxp cx] /BQ_P[py nyz dyp cy] le1] [_ _ le2]. move: le1 le2; rewrite /BQle_aux (BZprodC (P y))(BZprodC (Q y)) => la lb. move: (BZ_Bezout_if_coprime nxz (BZps_sBZ dxp) cx) => bx. move: (BZ_Bezout_if_coprime nyz (BZps_sBZ dyp) cy) => bzy. move:(zleA la lb) => eq1. move: (BQ_of_pair_prop2 nxz dxp nyz dyp bx bzy eq1) => [sc sd]. by apply: pair_exten. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)