proposition: Lemma fin_pickleK : pcancel fin_pickle fin_unpickle.
proof: Proof. move=> x; rewrite /fin_pickle/fin_unpickle. rewrite -(index_map Some_inj) nth_index ?map_f//. by apply/count_memPn=> /eqP; rewrite f. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)