proposition: Lemma seq_sub_pickleK : pcancel seq_sub_pickle seq_sub_unpickle.
proof: Proof. rewrite /seq_sub_unpickle => x. by rewrite (nth_map x) ?nth_index ?index_mem ?mem_seq_sub_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)