proposition: Lemma corner_box_in_part sh rc : corner_box sh rc -> in_shape sh rc.
proof: Proof. move: rc => [r c]. rewrite /corner_box /in_shape /is_rem_corner /= => /andP[Hr /eqP->]. by move: Hr; case (nth 0 sh r). Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure