proposition: Lemma sumList_series_split_first : forall n f, sumList (n :: getNats O n) f == f O + (sumList (getNats 1 n) f).
proof: Proof. induction n; intuition; unfold sumList in *; simpl in *. eapply ratAdd_comm. rewrite fold_add_body_eq. 2:{ rewrite ratAdd_assoc. rewrite ratAdd_comm. rewrite ratAdd_assoc. rewrite (ratAdd_comm (f n ) 0). eapply eqRat_refl. } rewrite fold_add_init. rewrite IHn. rewrite ratAdd_comm. eapply eqRat_trans. 2:{ symmetry. eapply ratAdd_eqRat_compat. eapply eqRat_refl. eapply eqRat_trans. eapply fold_add_body_eq. eapply ratAdd_comm. intuition. eapply eqRat_refl. eapply fold_add_init. } rewrite (ratAdd_comm (f (S n))). rewrite <- ratAdd_assoc. intuition. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation