proposition: Lemma sumnpSPE : (sumn p).-1.+1 = sumn p.
proof: Proof. Proof using Hcorn. have Hszp : (Alpha < size p)%N. move: Hcorn; rewrite /corner_box /is_rem_corner => /andP[H _]. move: H; apply contraLR; rewrite -!ltnNge ltnS => H. by rewrite (nth_default _ H). move: Hszp; case: p => /= [] [// | p0 p'] /part_head_non0 /=. by case: p0. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure