proposition: Fact Hp : incr_nth p' Alpha = p.
proof: Proof. Proof using Hcorn. exact: decr_nthK. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure