proposition: Lemma rat_inf_limit_sqrt: forall (f : nat -> Rat -> Prop) (v : Rat), rat_inf_limit f v -> rat_inf_limit (fun n => f (Nat.sqrt n)) v.
proof: Proof. intuition. eapply rat_inf_limit_mono. trivial. intuition. eapply Nat.sqrt_le_mono. trivial. intuition. econstructor. eapply Nat.sqrt_square. Qed.
imports: Arith FCF.Fold List FCF.StdNat FCF.Rat Arith