proposition: Lemma arm_length_corner_box sh r c u v : is_part sh -> r <= u -> c <= v -> corner_box sh (u, v) -> arm_length sh (r, c) = arm_length sh (u, c) + arm_length sh (r, v).
proof: Proof. move=> /is_part_ijP[_ Hpart]. rewrite /corner_box /is_rem_corner => Hr Hc /=/andP[Hcorn /eqP Hv]. subst v. rewrite /arm_length. move/(_ _ _ Hr): Hpart => {Hr}. move: Hc Hcorn; case: (nth 0 sh u) => // pu. rewrite [_.+1.-1]/= => Hcpu; rewrite (subSn Hcpu) => _ Hpu. have:= leq_ltn_trans Hcpu Hpu. case: (nth 0 sh r) Hpu => // pr. rewrite !ltnS => Hpu Hcpr. by rewrite !subSn //= addnC addnBA // subnK. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure