proposition: Lemma zlt_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:(zlt_P1 (BZ_of_natp_i aN)(BZ_of_natp_i bN)); rewrite !BZ_of_nat_val. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)