proposition: Lemma incr_nth_injl u v i : 0 \notin u -> 0 \notin v -> incr_nth u i = incr_nth v i -> u = v.
proof: Proof. move=> Hu Hv /eqP. elim: u v Hu Hv i => [/= v _ | u0 u IHu v] /=; case: v => [// | v0 v]. - rewrite inE negb_or => /andP[Hv0 _]. by case=> [| i] /= /eqP[H]; rewrite H eq_refl in Hv0. - move=> {IHu}. rewrite inE negb_or => /andP[Hu0 _] _. by case=> [| i] /= /eqP[H]; rewrite H eq_refl in Hu0. - rewrite !inE !negb_or => /andP[Hu0 Hu] /andP[Hv0 Hv]. case=> [| i] /= /eqP[->]; first by move ->. by move/eqP/(IHu _ Hu Hv) ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau