proposition: Lemma rat_inf_limit_ratInverse : forall (f : nat -> Rat -> Prop) a v, rat_inf_limit f a -> ~ a == 0 -> ratInverse a == v -> left_total f -> rat_inf_limit (fun n => ratInverse_rel (f n)) v.
proof: Proof. intuition. eapply rat_inf_limit_comp. eauto. symmetry. trivial. eapply ratInverse_continuous. trivial. trivial. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith