proposition: Lemma arm_length_incr_nth_row sh r c : in_shape sh (r, c) -> arm_length (incr_nth sh r) (r, c) = (arm_length sh (r, c)).+1.
proof: Proof. rewrite /in_shape /arm_length nth_incr_nth eq_refl add1n => Hc. rewrite prednK; last by rewrite subn_gt0. by rewrite subSn; last exact: ltnW. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure