proposition: Lemma enum_yamnE : map val (enum {:yamn}) = flatten [seq enum_yameval p | p <- enum_partn n].
proof: Proof. Proof using. rewrite enum_unionE /=; congr flatten. rewrite [LHS](eq_map (g := enum_yameval \o val)). - by rewrite map_comp enum_intpartnE. - by move=> i /=; rewrite enum_yamevalE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition