proposition: Lemma yamn_partition_evalseq yam : is_yam_of_size n yam -> (is_part_of_n n) (evalseq yam).
proof: Proof. Proof using. by rewrite /is_yam_of_size /= evalseq_eq_size => /andP[/is_part_eval_yam -> ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition