proposition: Lemma ends_at_rem_cornerE : (fun X : seq nat * seq nat => \sum_(i0 <- rem_corners p) (ends_at (i0, (nth O p i0).-1) X)%:Q) == (fun X => (corner_box p (last O X.1, last O X.2))%:Q).
proof: Proof. Proof using. rewrite /ends_at => [] [A B] /=. case (boolP (corner_box p (last O A, last O B))) => Hcorn. - rewrite (bigD1_seq (last O A) _ (rem_corners_uniq p)) /=; first last. move: Hcorn; rewrite /rem_corners /corner_box => /andP[Hcorn _]. rewrite mem_filter Hcorn mem_iota add0n leq0n /=. move: Hcorn; rewrite /is_rem_corner. by apply contraLR; rewrite -!ltnNge ltnS => /(nth_default O) ->. move: Hcorn; rewrite /corner_box eq_refl => /andP[_ ->] /=. by rewrite big1 // => i; rewrite eq_sym => /negbTE ->. - rewrite big_seq_cond big1 // => i. rewrite mem_filter andbT => /andP[Hout _]. suff /negbTE -> : ~~ ((last O A == i) && (last O B == (nth O p i).-1)) by []. move: Hcorn; rewrite /corner_box; apply contra => /andP[/eqP Hi]. by subst i => ->; rewrite Hout. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure