∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : ℕ → Submodule R M}
  (hp : Antitone p) (x : (n : ℕ) → M ⧸ p n),
  (∀ (m : ℕ), x m = (Submodule.factor ⋯) (x (m + 1))) → ∀ {m n : ℕ} (g : m ≤ n), x m = (Submodule.factor ⋯) (x n)