proposition: Lemma BZdvds_opp2 a b: intp a -> (b %|z a <-> b %|z (BZopp a)).
proof: Proof. move => az; move: (ZSo az) => oaz. split; move => h; move: (BZdvds_pr0 h) => h1;move: h=> [pa pb pc]. by apply/(BZdvds_pr3 oaz pb); rewrite BZopp_val. by apply /(BZdvds_pr3 az pb); rewrite -(BZopp_val a). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)