proposition: Lemma BZ_of_Z_opp x: BZ_of_Z (- x) = BZopp (BZ_of_Z x).
proof: Proof. case: x => p; simpl; last by rewrite BZopp_m //. by rewrite BZopp_p; case: p => //=; rewrite /BZm_of_nat; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)