proposition: Lemma isum_p7a n: (ipartial_sum (Zo E (fun t => glt r t n))) <=o ipartial_sum E.
proof: Proof. set I := Zo _ _. set J := E -s I. have sa: sub I E by apply:Zo_S. have sb: sub J E by apply:sub_setC. have sc i j :inc i I -> inc j J -> glt r i j. move => /Zo_P [iE la] /setC_P [jE ll]. case: (total_order_pr1 (worder_total wor) iE jE) => // lc; case: ll. apply:Zo_i=> //; apply:(lt_lt_trans (proj1 wor) lc la). apply:Zo_i=> //;ue. move: (isum_p4 sa sb sc); rewrite (setU2_Cr sa) => <-. by apply: osum_Mle0; apply: isum_p1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)