proposition: Lemma is_row_invins b s : is_row s -> is_row (invins b s).
proof: Proof. Proof using. rewrite /invins. elim: s => [_ // | l0 s IHs] /= /is_row_cons[Hhead Hrow]. case: (leP b (head b s)) => [| Hb] /=; first by move: Hrow; case s => [// | s0 s'] /= -> ->. move/(_ Hrow): IHs. case H : (invbumprow b s) => [[// | r0 r] a] /= ->; rewrite andbT. apply: (le_trans Hhead). have -> : r0 = head l0 (invins b s) by rewrite /invins H. case: (s =P [::]) => [-> // | /eqP Hnnil]. apply: (head_lt_invins _ Hnnil). by rewrite /invbump Hb. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab