proposition: Lemma hook_length_incr_nth_row sh r c : is_part sh -> is_add_corner sh r -> in_shape sh (r, c) -> hook_length (incr_nth sh r) (r, c) = (hook_length sh (r, c)).+1.
proof: Proof. rewrite /hook_length => Hpart Hcrn Hin; apply eq_S. rewrite (arm_length_incr_nth_row Hin) addSn. congr (_ + _).+1. rewrite /leg_length /arm_length (conj_part_incr_nth Hpart Hcrn) nth_incr_nth. move: Hin; rewrite /in_shape eq_sym ltn_neqAle => /andP[/negbTE -> _]. by rewrite add0n. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure