proposition: Lemma sumList_series_incr : forall n2 n1 (f f' : nat -> Rat), (forall n, (f n) == (f' (S n))) -> sumList (getNats n1 n2) f == sumList (getNats (S n1) n2) f'.
proof: Proof. induction n2; intuition; unfold sumList; simpl in *. intuition. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } rewrite fold_add_init. unfold sumList in *. rewrite IHn2; eauto. eapply eqRat_trans. 2:{ symmetry. eapply eqRat_trans. eapply fold_add_body_eq. eapply ratAdd_comm. intuition. eapply eqRat_refl. eapply fold_add_init. } eapply ratAdd_eqRat_compat. eauto. intuition. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation