proposition: Lemma leg_length_corner_box sh r c u v : is_part sh -> r <= u -> c <= v -> corner_box sh (u, v) -> leg_length sh (r, c) = leg_length sh (u, c) + leg_length sh (r, v).
proof: Proof. rewrite /leg_length addnC => Hpart Hru Hcv Hcorn. apply: (arm_length_corner_box (is_part_conj Hpart) Hcv Hru). exact: corner_box_conj_part. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure