I am trying to prove the following using the Mathematical Components library:
Lemma bigsum_aux (i: 'I_q) (j: 'I_q) (F G : 'I_q -> R):
(forall i0, F i0 <= G i0) /\ (exists j0, F j0 < G j0) ->
\sum_(i < q) F i < \sum_(i < q) G i.
Initially, I was trying to find some Lemma equivalent to bigsum_aux
in the documentation of ssralg
or bigop
, but I couldn't find any; so this is what I have been able to do so far:
Proof.
move => [Hall Hex]. rewrite ltr_neqAle ler_sum; last first.
- move => ? _. exact: Hall.
- rewrite andbT. (* A: What now? *)
Any help or pointers towards relevant lemmas would be welcome.
You want to split the sum in the "bad" (<) part, then the rest is trivial: