Theorem: SCF.FOR_PEELING.identity₁ (MLIR/Dialects/ScfSemantics.lean)

State before:
n : ℕ
⊢ Int.toNat (Int.ofNat n + 1 - 0) = n + 1
Tactic:
sorry
State after:
no goals