proposition: Lemma rat_inf_limit_squeeze : forall (f1 f2 f: nat -> Rat -> Prop) c (v : Rat), rat_inf_limit f1 v -> rat_inf_limit f2 v -> (forall n a a1, n >= c -> f n a -> f1 n a1 -> a1 <= a) -> (forall n a a2, n >= c -> f n a -> f2 n a2 -> a <= a2) -> left_total f1 -> left_total f2 -> rat_inf_limit f v.
proof: Proof. unfold rat_inf_limit, inf_limit in *. intuition. destruct (H epsilon); intuition. destruct (H0 epsilon); intuition. exists (max c (max x x0)). intuition. destruct (H3 n'). destruct (H4 n'). eapply leRat_trans. eapply ratDistance_le_max. eapply H1. eapply Nat.max_lub_l. eauto. eapply H9. eapply H10. eapply H2. eapply Nat.max_lub_l. eauto. eapply H9. eapply H11. eapply maxRat_leRat_same; eauto using Nat.max_lub_l, Nat.max_lub_r. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith