proposition: Lemma rat_inf_limit_const : forall (f : Rat -> Prop) a, f a -> (forall a1 a2, f a1 -> f a2 -> a1 == a2) -> rat_inf_limit (fun _ => f) a.
proof: Proof. unfold rat_inf_limit, inf_limit in *. intuition. exists O. intuition. eapply leRat_trans. eapply eqRat_impl_leRat. rewrite <- ratIdentityIndiscernables. eauto. eapply rat0_le_all. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith