proposition: Lemma rat_inf_limit_trans : forall (f1 f2 : nat -> Rat -> Prop) a, rat_inf_limit_2 f1 f2 -> rat_inf_limit f2 a -> left_total f2 -> rat_inf_limit f1 a.
proof: Proof. intuition. unfold rat_inf_limit_2, inf_limit_2, rat_inf_limit, inf_limit in *. intuition. edestruct (H (ratHalf epsilon)). eapply ratHalf_ne_0. intuition. edestruct (H0 (ratHalf epsilon)). eapply ratHalf_ne_0. intuition. exists (Nat.max x x0). intuition. destruct (H1 n'). eapply leRat_trans. eapply ratTriangleInequality. rewrite H3. rewrite H4. rewrite ratHalf_add. intuition. eapply Nat.max_lub_r. eauto. eauto. eapply Nat.max_lub_l. eauto. trivial. trivial. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith