proposition: Lemma eq_inv_is_row (d1 d2 : unit) (T1 : inhOrderType d1) (T2 : inhOrderType d2) (u1 : seq T1) (u2 : seq T2) : eq_inv u1 u2 -> is_row u1 -> is_row u2.
proof: Proof. move/eq_invP => [Hsz Hinv] /(is_rowP inh) Hrow. apply/(is_rowP inh) => i j; rewrite -Hsz => Hij. rewrite -(Hinv i j Hij). exact: Hrow. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau