proposition: Lemma BZdvds_pr3 a b: intp a -> intp b -> (b %|z a <-> (BZ_val b) %|c (BZ_val a)).
proof: Proof. move => az bz. split; [ by apply:BZdvds_pr0 | move => [sa sb sc] ]. case: (equal_or_not b \0z) => bnz. suff: a = \0z by move -> ; rewrite bnz;apply:BZdvds_trivial. by apply: (BZ_0_if_val0 az); rewrite - sc bnz BZ0_val (crem_zero sa). split => //; exact:(BZrem_div1 az bz bnz sc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)