proposition: Lemma leR_sumR_predU (A : finType) (f : A -> R) (P Q : pred A) : (forall a, 0 <= f a) -> \sum_(i in A | [predU P & Q] i) f i <= \sum_(i in A | P i) f i + \sum_(i in A | Q i) f i.
proof: Proof. move=> Hf. elim: (index_enum _) => [|h t IH /=]; first by rewrite !big_nil /=; Lra.lra. rewrite !big_cons /=. case: ifPn => /=. - case/orP => [hP | hQ]. + move: hP; rewrite unfold_in => ->. case: ifP => // Qh. * rewrite -addRA; apply leR_add2l. apply (leR_trans IH). have : forall a b c, 0 <= c -> a + b <= a + (c + b) by move=> *; Lra.lra. apply; by apply Hf. * rewrite -addRA; apply leR_add2l. exact/(leR_trans IH)/Req_le. + move: hQ; rewrite unfold_in => ->. case: ifP => // Ph. * rewrite -addRA; apply/leR_add2l/(leR_trans IH). have : forall a b c, 0 <= c -> a + b <= a + (c + b) by move=> *; Lra.lra. apply; by apply Hf. * rewrite -(addRC (f h + _)) -addRA; apply/leR_add2l/(leR_trans IH). by rewrite addRC; apply Req_le. - rewrite negb_or. case/andP. rewrite !unfold_in; move/negbTE => -> /negbTE ->. exact/IH. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)