proposition: Lemma BZ_of_div (a b:nat): a %| b <-> (BZ_of_Z a) %|z (BZ_of_Z b).
proof: Proof. move: (nat_to_B_Nat a) (nat_to_B_Nat b) => aN bN. move:(BZdiv_cN aN bN) => H. split => dvd. apply/H; move/dvdnP:dvd => [k ->]. rewrite nat_to_B_prod cprodC; apply: cdivides_pr1 => //. apply:nat_to_B_Nat. move/H: dvd => / cdivides_pr. move: (NS_quo (nat_to_B a) bN) => /nat_to_B_surjective [k ->]. rewrite -nat_to_B_prod => /nat_to_B_injective ->. by apply/dvdnP; exists k; rewrite mulnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)