∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsPrecomplete I M ↔
    ∀ (f : ℕ → M), (∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD I ^ m • ⊤]) → ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD I ^ n • ⊤]