proposition: Lemma arm_length_ler sh r c j : is_part sh -> r < j -> in_shape sh (j, c) -> arm_length sh (j, c) <= arm_length sh (r, c).
proof: Proof. rewrite /in_shape /arm_length => /is_part_ijP[_ Hpart] Hr Hc. move/(_ _ _ (ltnW Hr)): Hpart => Hshjr. rewrite -ltnS !prednK; first exact: leq_sub2r. - by rewrite subn_gt0; apply: leq_trans Hc Hshjr. - by rewrite subn_gt0; apply: Hc. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure