proposition: Lemma rat_inf_limit_exp_0 : forall (f : nat -> Rat -> Prop) a, rat_inf_limit f a -> ~ 1 <= a -> (forall n, exists r, f n r) -> rat_inf_limit (fun n => (expRat_rel (f n) n)) 0.
proof: Proof. intuition. unfold rat_inf_limit, inf_limit in *. intuition. edestruct (H (1 / 2 * (ratSubtract 1 a))); eauto. intuition. apply ratMult_0 in H3. intuition. eapply H0. eapply ratSubtract_0_inv. trivial. edestruct (@expRat_le_exp_exists (a + (1 / 2) * (ratSubtract 1 a)) epsilon). eapply half_distance_1_le; trivial. trivial. exists (Nat.max x x0). intuition. unfold expRat_rel in *. destruct (H1 n'). rewrite H6; eauto. apply ratDistance_0_r_le. eapply leRat_trans. eapply expRat_leRat_compat. eapply ratDistance_le_sum. eapply H3. eapply Nat.max_lub_l. eauto. trivial. eapply expRat_le'. eauto. eapply half_distance_1_le; trivial. eapply Nat.max_lub_r. eauto. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith