proposition: Lemma iotagtnk k : [seq x <- iota 0 N | gtn k x] = iota 0 (minn N k).
proof: Proof. Proof using. rewrite /minn; case ltnP => Hn. - rewrite (eq_in_filter (a2 := predT)); first by rewrite filter_predT. move=> i; rewrite mem_iota add0n /= => Hi. by rewrite (ltn_trans Hi Hn). - rewrite -{1}[k]addn0; move: (0%N) => i. elim: k i N Hn => [/= | k IHk] i n Hn. + rewrite (eq_in_filter (a2 := pred0)); first by rewrite filter_pred0. by move=> j; rewrite mem_iota leqNgt add0n => /andP[/negbTE ->]. + have:= ltn_predK Hn => H; rewrite -H in Hn. move/(_ i.+1 _ Hn): IHk => /= <-. by rewrite -{1}H /= -{1}[i]add0n ltn_add2r /= addSnnS. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype