proposition: Fact Hpart' : is_part p'.
proof: Proof. Proof using Hcorn. exact: is_part_decr_nth. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure