proposition: Lemma mask_enum_ord m : mask m (enum 'I_n) = [seq i <- enum 'I_n | nth false m (val i)].
proof: Proof. rewrite mask_filter ?enum_uniq//; apply: eq_filter => i. by rewrite in_mask ?enum_uniq ?mem_enum// index_enum_ord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)