proposition: Lemma rat_inf_limit_comp : forall (f : nat -> Rat -> Prop)(g : Rat -> Rat -> Prop) a v, rat_inf_limit f a -> g a v -> continuous_at g a -> left_total f -> rat_inf_limit (fun n r => forall v', (f n v' -> g v' r)) v.
proof: Proof. unfold continuous_at, rat_limit, rat_inf_limit, inf_limit in *. intuition. edestruct H1; eauto. intuition. destruct (H x). trivial. exists x0. intuition. destruct (H2 n'). eapply H6. eauto. eapply H4. eapply H7. trivial. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith