proposition: Lemma size_ins_non_0 : 0 < size ins.
proof: Proof. Proof using. by move: ins_non_nil; case ins. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab