proposition: Lemma toZp_eq n (x y: BITS n) : (x == y) = (toZp x == toZp y).
proof: Proof. destruct n. by rewrite (tuple0 x) (tuple0 y). case E: (toZp x == toZp y). rewrite (toZp_inj (eqP E)). by rewrite eq_refl. apply (contraFF (b:=false)) => // => H. rewrite (eqP H) (eq_refl) in E. done. 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