proposition: Lemma toZpK n : cancel (@toZp n) (@fromZp n).
proof: Proof. case E: (n == 0). + rewrite /cancel. rewrite (eqP E). move => x. apply trivialBits. + move => x. rewrite /fromZp/toZp/=. rewrite Zp_cast. by rewrite (modn_small (toNatBounded _)) toNatK. apply negbT in E. destruct n => //. apply pow2_gt1. 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