∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] [NonarchimedeanAddGroup G]
  {f : ℕ → G}, Filter.Tendsto (fun n => f (n + 1) - f n) Filter.atTop (nhds 0) → CauchySeq f