proposition: Corollary toZp_neq n (x y: BITS n) : (x != y) = (toZp x != toZp y).
proof: Proof. by rewrite toZp_eq. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec