proposition: Lemma BZdvds_opp1 a b: intp b -> (b %|z a <-> (BZopp b) %|z a).
proof: Proof. move => bz; move: (ZSo bz) => obz. split;move=> [pa pb pc]; hnf. by rewrite /BZdivides (BZrem_opp_b pa pb). by rewrite -(BZrem_opp_b pa bz) pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)