proposition: Lemma z_codeK : pcancel z_code z_decode.
proof: Proof. rewrite /z_code /z_decode. case=> // n; case e : (pickle n)=>[|m]; rewrite -?e ?pickleK //; by move/ltP: (lt_O_nat_of_P n); rewrite -e -[pickle]/nat_of_P ltnn. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrnat seq order) mathcomp(choice fintype finfun ssrfun bigop ssralg) Zbool Qcanon ZArith