proposition: Lemma BZopp_m x: BZopp (BZm_of_nat x) = BZ_of_nat x.
proof: Proof. rewrite /BZm_of_nat; Ytac bz; first by rewrite BZopp_0 bz. by rewrite /BZopp/int_np; aw; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)