fact: Definition adhoc_seq_sub_countType := HB.pack_for countType seq_sub seq_sub_isCountable (Choice.class adhoc_seq_sub_choiceType).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)