proposition: Lemma hook_length_last_rectangle (a b : nat) (A B : seq nat) : is_trace (a :: A) (b :: B) -> hook_length p (a, b) = hook_length p (last a A, b) + hook_length p (a, (last b B)) - 1.
proof: Proof. Proof using. rewrite /is_trace => /and5P[_ _ HA HB /=]. exact: hook_length_corner_box (sorted_leq_last HA) (sorted_leq_last HB). Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure