proposition: Lemma hook_length_incr_nth sh i r c : is_part sh -> is_add_corner sh i -> in_shape sh (r, c) -> i != r -> nth 0 sh i != c -> hook_length (incr_nth sh i) (r, c) = hook_length sh (r, c).
proof: Proof. rewrite /hook_length => Hpart Hcorn Hin Hr Hc; apply eq_S. congr (_ + _). - exact: arm_length_incr_nth_nrow. - rewrite /leg_length conj_part_incr_nth //. exact: arm_length_incr_nth_nrow. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure