proposition: Lemma fold_add_matchOrder : forall (A : Set)(ls : list A)(f : A -> Rat) n init1 init2, init1 == init2 -> NoDup ls -> (forall a, In a ls -> (~In a (firstn n ls)) -> (f a) == 0) -> fold_left (fun r a => r + (f a)) (firstn n ls) init1 == fold_left (fun r a => r + (f a)) ls init2.
proof: Proof. induction ls; intuition; simpl in *. destruct n; simpl in *; trivial. inversion H0; clear H0; subst. destruct n; simpl in *. eapply eqRat_symm. eapply eqRat_trans. eapply fold_add_eq_init_f; intuition. rewrite (ratAdd_0_r init1). eapply ratAdd_eqRat_compat; intuition. eapply IHls. eapply ratAdd_eqRat_compat; intuition. trivial. intuition. eapply H1. intuition. intuition. subst. intuition. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation