proposition: Lemma rat_inf_limit_div_2 : forall (f : nat -> Rat -> Prop)(v : Rat), rat_inf_limit f v -> rat_inf_limit (fun n => (f (Nat.div2 n))) v.
proof: Proof. unfold rat_inf_limit, inf_limit. intuition. destruct (H epsilon); intuition. econstructor. intuition. specialize (H1 (Nat.div2 n')). eapply H1. eapply div2_ge; eauto. eauto. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith