∀ {R : Type u₁} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] {f : Ring.Perfection R p}
  {m n : ℕ}, (Perfection.coeff R p m) f ≠ 0 → m ≤ n → (Perfection.coeff R p n) f ≠ 0