proposition: Lemma sumList_rel_sumList : forall (A : Set)(ls : list A)(f : A -> Rat), sumList_rel (fun a r => f a = r) ls (sumList ls f).
proof: Proof. induction ls; intuition. unfold sumList. simpl. econstructor. intuition. unfold sumList in *. simpl in *. econstructor. eapply IHls. eauto. rewrite fold_add_body_eq. 2:{ eapply ratAdd_comm. } rewrite fold_add_init. eapply eqRat_refl. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation