English
For any f and n, trunc (n-1) (d/dX f) = polynomial derivative of trunc n f; with the n=0 case treated separately.
Русский
Для любых f и n: trunc (n-1) (d/dX f) = derivative (trunc n f); при n=0 это тривиально.
LaTeX
$$$ \\operatorname{trunc}_{n-1}\\big( \\tfrac{d}{dX} f \\big) = \\operatorname{derivative}( \\operatorname{trunc}_n f ) \quad( n \\in \\mathbb{N})$$$
Lean4
theorem trunc_derivative' (f : R⟦X⟧) (n : ℕ) : trunc (n - 1) (d⁄dX R f) = Polynomial.derivative (trunc n f) := by
cases n with
| zero => simp
| succ n => rw [succ_sub_one, trunc_derivative]