proposition: Lemma hook_length_incr_nth_col sh r i : is_part sh -> is_add_corner sh r -> in_shape sh (i, (nth 0 sh r)) -> hook_length (incr_nth sh r) (i, nth 0 sh r) = (hook_length sh (i, nth 0 sh r)).+1.
proof: Proof. move=> Hpart Hcorn Hin. rewrite -hook_length_conj_part; last exact: is_part_incr_nth. rewrite conj_part_incr_nth // hook_length_incr_nth_row; first last. - by rewrite -in_conj_part. - exact: is_add_corner_conj_part. - exact: is_part_conj. by rewrite hook_length_conj_part. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure