proposition: Lemma fold_add_body_const : forall (A : Set)(ls : list A) c init, fold_left (fun r a => r + c) ls init == c * (length ls / 1) + init.
proof: Proof. induction ls; intuition; simpl in *. eapply eqRat_trans. eapply ratAdd_0_l. eapply ratAdd_eqRat_compat. eapply eqRat_symm. apply ratMult_0_r. intuition. rewrite IHls. eapply eqRat_trans. eapply ratAdd_eqRat_compat. apply eqRat_refl. apply ratAdd_comm. rewrite <- (ratAdd_assoc). apply ratAdd_eqRat_compat; intuition. eapply eqRat_symm. eapply eqRat_trans. eapply ratMult_eqRat_compat. apply eqRat_refl. apply ratS_num. rewrite ratMult_distrib. rewrite ratAdd_comm. apply ratAdd_eqRat_compat; intuition. apply ratMult_1_r. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool