proposition: Lemma is_yamP s : reflect (forall i n, count_mem n (drop i s) >= count_mem n.+1 (drop i s)) (is_yam s).
proof: Proof. apply (iffP idP). - elim: s => //= s0 s IHs /andP[/is_partP[_ Hpart] {}/IHs Hrec]. case => [| i] n //=. case: (s0 =P n) => Hns0. + subst s0; rewrite ltn_eqF // add0n add1n. by move/(_ 0 n) : Hrec; rewrite drop0 => /leq_trans; apply. + case: (s0 =P n.+1) => Hn1s0. move/(_ n) : Hpart; rewrite !nth_incr_nth Hn1s0 eq_refl eq_sym ltn_eqF //. by rewrite !add0n !add1n !nth_evalseq. + by move/(_ 0 n) : Hrec; rewrite !add0n drop0. - elim: s => // s0 s IHs H. apply/andP; split. + move: (s0 :: s) {IHs} H => {s0}s /(_ 0); rewrite drop0 => Hs. apply /is_partP; split; last by move=> i; rewrite !nth_evalseq. elim: s {Hs} => //= s0 s IHs. exact: last_incr_nth_non0. + apply: IHs => i n; exact (H i.+1 n). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition