proposition: Lemma arm_length_incr_nth_nrow sh r c i : i != r -> arm_length (incr_nth sh i) (r, c) = arm_length sh (r, c).
proof: Proof. rewrite /arm_length nth_incr_nth => /negbTE ->. by rewrite add0n. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure