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