proposition: Lemma BZdiv_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. move:(BZdvds_pr3 (BZ_of_nat_i bN) (BZ_of_nat_i aN)). by rewrite !BZ_of_nat_val. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)