proposition: Lemma nbump_size_ins : ~~bump -> size ins = (size Row).+1.
proof: Proof. Proof using HRow. move/nbump_mininspredE => H. by rewrite -insE /insmin size_set_nth maxnC /maxn H ltnSn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab