proposition: Lemma zle_P1 x y: inc x BZp -> inc y BZp -> (x <=z y <-> (BZ_val x) <=c (BZ_val y)).
proof: Proof. move => pa pb; move: (BZp_sg pa) (BZp_sg pb) => pc pd. move:(BZp_sBZ pa) (BZp_sBZ pb) => pa' pb'. split. move=> [_ _]; rewrite /int_np pc; by case; move => [ba] => //; case:C0_ne_C1. by move => h; split => //; constructor 3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)