proposition: Lemma fromZpK n : cancel (@fromZp n.+1) (@toZp n.+1).
proof: Proof. move => x. rewrite /toZp/fromZp. rewrite toNat_fromNat modn_small. apply valZpK. destruct x. simpl. rewrite Zp_cast in i => //. 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