proposition: Lemma val_sub_enum : map val sub_enum = enum P.
proof: Proof. rewrite pmap_filter; last exact: insubK. by apply: eq_filter => x; apply: isSome_insub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)