proposition: Lemma in_hook_boxesP rc kl : (kl \in hook_boxes rc) = (in_hook rc kl).
proof: Proof. Proof using. move: rc kl => [r c] [k l] /=. apply/mapP/idP => /= [|]. - move=> /= [[]x]; rewrite mem_cat => /orP[] /=. + rewrite mem_map; last by move=> u v []. rewrite mem_iota => /andP[Hrx Hxr] /=[->{k} ->{l}]. rewrite /in_hook; apply/orP; right. by rewrite eq_refl Hrx /= -(iota_hookE _ Hrx). + by move=> /mapP[y] _. + by move=> /mapP[y] _. + rewrite mem_map; last by move=> u v []. rewrite mem_iota => /andP[Hcx Hxc] /= [->{k} ->{l}]. rewrite /in_hook; apply/orP; left. by rewrite eq_refl Hcx /= -(iota_hookE _ Hcx). - rewrite /in_hook => /orP[] /and3P[/eqP <-]. + move=> {k} Hc Hr. exists (inr l); last by []. rewrite mem_cat; apply/orP; right; rewrite mem_map; last by move=> u v []. by rewrite mem_iota Hc /= iota_hookE. + move=> {l} Hr Hc. exists (inl k); last by []. rewrite mem_cat; apply/orP; left; rewrite mem_map; last by move=> u v []. by rewrite mem_iota Hr /= iota_hookE. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure