proposition: Lemma yamn_PredEq (ev : intpartn n) : predI (is_yam_of_size n) (pred1 (val ev) \o evalseq) =1 is_yam_of_eval (val ev).
proof: Proof. Proof using. move=> y; rewrite /is_yam_of_size /is_yam_of_eval /= -andbA; congr (_ && _). case: (evalseq y =P ev) => /=; last by rewrite andbF. rewrite -evalseq_eq_size => ->. by rewrite (sumn_intpartn ev) eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition