proposition: Lemma append_nth_injl d (T : inhOrderType d) (u v : seq (seq T)) (l : T) p : [::] \notin u -> [::] \notin v -> append_nth u l p = append_nth v l p -> u = v.
proof: Proof. move=> /shape0 Hu /shape0 Hv Heq; have:= congr1 shape Heq. rewrite !shape_append_nth => /(incr_nth_injl Hu Hv) /eqP {Hu Hv}. move: Heq; rewrite /append_nth. elim: u v p => [| u0 u IHu] /=; case=> [| v0 v] //=. case=> [| p] /= []; first by move/rconsK => -> ->. by move=> -> Heq /eqP[] /eqP /(IHu _ _ Heq) ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau