proposition: Lemma ltn_sum [I : eqType] (r : seq I) [P : pred I] [E1 E2 : I -> nat] (x : I) : (forall i : I, P i -> i !=x -> E1 i <= E2 i) -> x \in r -> P x -> E1 x < E2 x -> \sum_(i <- r | P i) E1 i < \sum_(i <- r | P i) E2 i.
proof: Proof. move=> leE12 x_r Px lt_x; rewrite !(big_rem x x_r) Px /= -addSn leq_add //. apply: leq_sum => i Pi; have [->|] := eqVneq i x;[exact: ltnW| exact: leE12]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)