mimick ler_sum and ler_sum_nat from ssrnum for improved forward compat

CHANGELOG_UNRELEASED.md

@@ -52,7 +52,7 @@
            `ler0_derive1_nincrNy`, `ger0_derive1_ndecrNy`
   + lemmas `ltr0_derive1_decr`, `gtr0_derive1_incr`
 - in `mathcomp_extra.v`:
-  + lemma `ltr_sum`
+  + lemmas `size_filter_gt0`, `ltr_sum`, `ltr_sum_nat`
 
 - in `classical_sets.v`:
   + lemma `itv_sub_in2`

classical/mathcomp_extra.v

@@ -590,13 +590,26 @@ by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT.
 Qed.
 
 (* TODO: move to ssrnum *)
-Lemma ltr_sum {R : numDomainType} {I : eqType} (r : seq I) (F G : I -> R) :
-  (0 < size r)%N -> (forall i, i \in r -> F i < G i) ->
-  \sum_(i <- r) F i < \sum_(i <- r) G i.
-Proof.
-elim: r => // h [|a t] ih _ FG.
-  by rewrite !big_cons !big_nil !addr0 FG// mem_head.
-rewrite [ltLHS]big_cons [ltRHS]big_cons ltrD//.
-  by rewrite FG// mem_head.
-by rewrite ih// => i iat; rewrite FG// inE iat orbT.
+
+Lemma size_filter_gt0 T P (r : seq T) : (size (filter P r) > 0)%N = (has P r).
+Proof. by elim: r => //= x r; case: ifP. Qed.
+
+Lemma ltr_sum [R : numDomainType] [I : Type] (r : seq I)
+    [P : pred I] [F G : I -> R] :
+  has P r ->
+  (forall i : I, P i -> F i < G i) ->
+  \sum_(i <- r | P i) F i < \sum_(i <- r | P i) G i.
+Proof.
+rewrite -big_filter -[ltRHS]big_filter -size_filter_gt0.
+case: filter (filter_all P r) => //= x {}r /andP[Px Pr] _ ltFG.
+rewrite !big_cons ltr_leD// ?ltFG// -(all_filterP Pr) !big_filter.
+by rewrite ler_sum => // i Pi; rewrite ltW ?ltFG.
+Qed.
+
+Lemma ltr_sum_nat [R : numDomainType] [m n : nat] [F G : nat -> R] :
+  (m < n)%N -> (forall i : nat, (m <= i < n)%N -> F i < G i) ->
+  \sum_(m <= i < n) F i < \sum_(m <= i < n) G i.
+Proof.
+move=> lt_mn i; rewrite big_nat [ltRHS]big_nat ltr_sum//.
+by apply/hasP; exists m; rewrite ?mem_index_iota leqnn lt_mn.
 Qed.

theories/realfun.v

@@ -2830,9 +2830,8 @@ have fin_S m : finite_set (S m).
     by rewrite ltr_pdivlMl// -natrM ltr_nat.
   rewrite card_fset_sum1 natr_sum mulr_sumr mulr1 big_tnth cardfE.
   rewrite -(big_mkord xpredT (fun=> m.+1%:R^-1)) size_sort cardfE.
-  apply: ltr_sum.
-    by rewrite size_iota subn0 -cardfE (leq_trans _ mFbFaB).
-  move=> /= k; rewrite mem_index_iota leq0n/= => kB.
+  rewrite ltr_sum_nat//; first by rewrite -cardfE (leq_trans _ mFbFaB).
+  move=> k; rewrite leq0n/= => kB.
   have : nth b s k \in S m.
     apply/mem_set/BSm => /=; rewrite -(@mem_sort _ <=%R).
     by apply/mem_nth; rewrite size_sort cardfE.