test: update `sym_simp_cd` test for perm theorem support Replace `Nat.add_comm_of_pos` (a permutation theorem) with `f_idem` (a non-perm conditional rewrite: `a > 0 → f (f a) = f a`). Update all examples and expected trace output accordingly. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.