proposition: Lemma corner_leg_length0 sh rc : is_part sh -> corner_box sh rc -> leg_length sh rc = 0.
proof: Proof. move: rc => [r c]; rewrite /leg_length => Hpart Hcorn. apply (corner_arm_length0 (is_part_conj Hpart)). exact: corner_box_conj_part. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure