proposition: Lemma is_yam_ijP s : reflect (forall d i j, i <= j -> count_mem i (drop d s) >= count_mem j (drop d s)) (is_yam s).
proof: Proof. apply (iffP idP). - move=> /is_yamP Hyam d i j Hij. move/(_ d) : Hyam => Hsuff. rewrite -(subnKC Hij). elim: (j-i) => [| r IHr]; first by rewrite addn0. apply: (leq_trans _ IHr). by rewrite addnS; exact: Hsuff. - by move=> H; apply/is_yamP => i d; exact: H. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass partition