proposition: Lemma hook_length_pred sh rc : (hook_length sh rc)%:~R - 1 = ((hook_length sh rc).-1)%:~R :> rat.
proof: Proof. by rewrite predn_int // !mulrzDr_tmp. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure