proposition: Lemma pickle_invK : ocancel pickle_inv pickle.
proof: Proof. by rewrite /pickle_inv => n; case def_x: (unpickle n) => //= [x]; case: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)