proposition: Lemma is_trace_corner_nil (a b : nat) (A B : seq nat) : is_trace (a :: A) (b :: B) -> (size (hook_box_indices (a, b)) == 0) = (A == [::]) && (B == [::]).
proof: Proof. Proof using. rewrite size_hook_box_indices. move=> Htrace; apply/idP/idP. - move=> /eqP Hal. have:= size_tracel Htrace; have:= size_tracer Htrace. move: Hal; rewrite /hook_length /= => ->. by rewrite !ltnS !leqn0 => /nilP -> /nilP ->. - move=> /andP/=[/eqP HA /eqP HB]; subst. move: Htrace => /and5P[_ _ _ _ /=]. rewrite /corner_box /hook_length /leg_length /arm_length /is_rem_corner. move => /andP/=[Ha /eqP Hb]; subst. have -> : (nth 0 p a - (nth 0 p a).-1) = 1. move: Ha; case: (nth 0 p a) => [// | pa] _. by rewrite /= subSn // subnn. rewrite /= add0n. suff -> : nth 0 conj (nth 0 p a).-1 = a.+1 by rewrite subSn // subnn. apply/eqP; rewrite nth_conjE //. move: Ha; case: (nth 0 p a) => [// | pa]. by rewrite !ltnS => -> /=. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure