proposition: Fact Hcrn : is_rem_corner p Alpha.
proof: Proof. Proof using Hcorn. by have:= Hcorn => /andP[Hcrn /eqP HBeta]. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure