proposition: Lemma z_pick_cancel : pcancel z_pickle z_unpickle.
proof: Proof. by move=> x; rewrite /z_pickle /z_unpickle pickleK z_codeK. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith