proposition: Lemma leg_length_ltr sh r c j : is_part sh -> r < j -> in_shape sh (j, c) -> leg_length sh (j, c) < leg_length sh (r, c).
proof: Proof. rewrite /leg_length => Hpart Hr. rewrite (in_conj_part Hpart). exact: (arm_length_ltl (is_part_conj _)). Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure