proposition: Lemma zle_cN a b: natp a -> natp b -> (a <=c b <-> BZ_of_nat a <=z BZ_of_nat b).
proof: Proof. move => aN bN;apply: iff_sym. by move:(zle_P1 (BZ_of_natp_i aN)(BZ_of_natp_i bN)); rewrite !BZ_of_nat_val. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)