proposition: Lemma BZdvds_pr6 a b: intp a -> intp b -> (a %|z b <-> sub (BZ_ideal1 b)(BZ_ideal1 a)).
proof: Proof. move => az bz; split. move => d1 x /funI_P [y yz ->]. rewrite (BZdvds_pr d1) -( BZprodA az (ZS_quo bz az) yz); apply /funI_P. by exists ((b %/z a) *z y) => //; apply: ZSp=> //; apply: ZS_quo. move=> h; move: (h _ (proj2 (BZ_in_ideal4 bz))) => /funI_P [z zz ->]. rewrite BZprodC; apply: (BZdvds_pr1 zz az). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)