proposition: Lemma ler_sum_nat (m n : nat) (F G : nat -> R) : (forall i, (m <= i < n)%N -> F i <= G i) -> \sum_(m <= i < n) F i <= \sum_(m <= i < n) G i.
proof: Proof. by move=> le_FG; rewrite !big_nat ler_sum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)