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