proposition: Lemma in_hook_shape rc kl : in_shape p rc -> in_hook rc kl -> in_shape p kl.
proof: Proof. Proof using. move: rc kl => [r c][k l]. rewrite /in_shape /in_hook => /= Hj /orP[] /and3P[/eqP <- // H1 H2]. by rewrite conj_ltnE. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure