proposition: Lemma ZSo x: intp x -> intp (BZopp x).
proof: Proof. move => xz; move: (BZ_valN xz) => pB. rewrite /BZopp; Ytac aux; [ by apply:BZ_of_nat_i | by apply:BZm_of_nat_i ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)