proposition: Lemma rat_inf_limit_sum : forall (f1 f2 : nat -> Rat -> Prop) v1 v2, left_total f1 -> left_total f2 -> rat_inf_limit f1 v1 -> rat_inf_limit f2 v2 -> rat_inf_limit (fun n => (ratAdd_rel (f1 n) (f2 n))) (v1 + v2).
proof: Proof. unfold rat_inf_limit, inf_limit in *. intuition. edestruct (H1 (ratHalf epsilon)). eapply ratHalf_ne_0. intuition. edestruct (H2 (ratHalf epsilon)). eapply ratHalf_ne_0. intuition. exists (Nat.max x x0). intuition. unfold ratAdd_rel in *. destruct (H n'). destruct (H0 n'). rewrite H7; eauto. eapply leRat_trans. eapply rat_distance_of_sum. rewrite H4. rewrite H5. rewrite ratHalf_add. intuition. eapply Nat.max_lub_r. eauto. trivial. eapply Nat.max_lub_l. eauto. trivial. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith