proposition: Lemma hook_length_corner_box sh r c u v : is_part sh -> r <= u -> c <= v -> corner_box sh (u, v) -> hook_length sh (r, c) = hook_length sh (u, c) + hook_length sh (r, v) - 1.
proof: Proof. move=> Hpart Hru Hcv Hcorn. rewrite /hook_length (arm_length_corner_box Hpart Hru Hcv Hcorn). rewrite (leg_length_corner_box Hpart Hru Hcv Hcorn). rewrite addSn subn1 /= !addnS !addnA; congr (_ + _).+1. by rewrite -!addnA; congr (_ + _); rewrite addnC. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure