proposition: Lemma zle_P3 x y: inc x BZms -> inc y BZms -> (x <=z y <-> (BZ_val y) <=c (BZ_val x)).
proof: Proof. move => pa pb; move: (BZms_sg pa) (BZms_sg pb) => pc pd. move:(BZms_sBZ pa) (BZms_sBZ pb) => pa' pb'. split. by move => [_ _]; rewrite/int_pp pd; case => [][aa bb] //; case:C0_ne_C1. by move=> h; split => //; constructor 1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)