proposition: Lemma qleT y x z: x <=q y -> y <=q z -> x <=q z.
proof: Proof. move => [xq yq le1] [_ zq le2]; split => //. move/BQ_P: xq => [_ pax pbx _]. move/BQ_P: yq => [_ pay pby _]. move/BQ_P: zq => [_ paz pbz _]. have pcx := BZps_sBZ pbx. have pcy := BZps_sBZ pby. have pcz := BZps_sBZ pbz. red in le1; red in le2. move: (BZprod_Mlege0 (BZps_sBZp pbz) le1). rewrite (BZprodC (P x)) - BZprodA // (BZprodC (Q y)) => le3. move: (BZprod_Mlege0 (BZps_sBZp pbx) le2). rewrite - BZprodA // - BZprodA // (BZprodC (Q y)). rewrite(BZprodC (Q z)) BZprodA // (BZprodC (P y)) (BZprodC _ (Q x)) => le4. by move/ (BZprod_ple2r (ZSp pax pcz) (ZSp pcx paz) pby):(zleT le3 le4). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)