proposition: Lemma head_instab (t0 : seq T) t l : is_row t0 -> head [::] (instab (t0 :: t) l) = ins t0 l.
proof: Proof. Proof using. move=> Hrow; rewrite -(insE Hrow) (insrowE Hrow). by rewrite ins_bumprowE /=; case (bumprow t0 l) => [[l'|]] b. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab