proposition: Lemma rat_inf_limit_summation : forall (A : Set)(f1 : A -> nat -> Rat -> Prop)(f2 : A -> Rat)(ls : list A), (forall a, rat_inf_limit (f1 a) (f2 a)) -> (forall a, left_total (f1 a)) -> (forall a n r1 r2, f1 a n r1 -> f1 a n r2 -> r1 == r2) -> rat_inf_limit (fun n : nat => sumList_rel (fun a0 : A => f1 a0 n) ls) (sumList ls f2).
proof: Proof. induction ls; intuition. unfold rat_inf_limit, inf_limit. intuition. exists O. intuition. inversion H4; clear H4; subst. unfold sumList. simpl. rewrite H5. eapply leRat_trans. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. intuition. eapply rat0_le_all. eapply (@rat_inf_limit_trans _ (fun n : nat => ratAdd_rel (f1 a n) (sumList_rel (fun a0 : A => f1 a0 n) ls))). unfold rat_inf_limit_2, inf_limit_2. intuition. exists O. intuition. inversion H5; clear H5; subst. unfold ratAdd_rel in *. rewrite H6. rewrite H12. eapply leRat_trans. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. eapply eqRat_refl. eapply rat0_le_all. trivial. trivial. eapply rat_inf_limit_eq. eapply rat_inf_limit_sum. eauto. unfold left_total; intuition. eapply sumList_rel_left_total. intuition. eapply H0. eapply H. eauto. unfold sumList. simpl. symmetry. rewrite fold_add_body_eq; [idtac | eapply ratAdd_comm | idtac]. rewrite fold_add_init. eapply eqRat_refl. intuition. unfold left_total; intuition. eapply ratAdd_rel_left_total. eapply H0. eapply sumList_rel_left_total. intuition. eapply H0. eauto. intuition. eapply sumList_rel_func; eauto. intuition. eauto. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith