proposition: Lemma BZdvd_opp a: intp a -> a <> \0z -> (a %|z (BZopp a) /\ (BZopp a) %/z a = \1mz).
proof: Proof. move => az anz;move: (BZdvd_itself az anz) => [pa pb]. rewrite (BZquo_opp2 pa) pb BZopp_1. split; [ by move/ (BZdvds_opp2 a az): pa | done]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)