proposition: Lemma BZquo_opp2 a b: b %|z a -> (BZopp a) %/z b = BZopp (a %/z b).
proof: Proof. move => h; move: (BZdvds_pr0 h) => [_ _ h1]; move: h => [az pb pc]. case: (equal_or_not b \0z) => bnz; first by rewrite bnz !BZ_quo0 BZopp_0. by apply: BZquo_opp_a1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)