proposition: Fact seq_sub_axiom : Finite.axiom seq_sub_enum.
proof: Proof. exact: Finite.uniq_enumP (undup_uniq _) mem_seq_sub_enum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)