theorem proved wrapper

`natCost_self`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  17@[simp] theorem natCost_self (n : Nat) : natCost n n = 0 := by

One-line wrapper that applies simp.

  18  simp [natCost]
  19

From the project-wide theorem graph. These declarations reference this one in their body.

natOrderedRealization in IndisputableMonolith.Foundation.OrderedLogicRealization decl_use

Lean names referenced from this declaration's body.