proposition: Lemma ins_head_lt : (head l ins <= l)%O.
proof: Proof. Proof using HRow. by rewrite -insE insrowE; exact: insrow_head_lt. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab