theorem other other

`toNat_succ`

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

formal statement (Lean)

 231@[simp] theorem toNat_succ (n : LogicNat) : toNat (succ n) = Nat.succ (toNat n) := rfl

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

fromNat_toNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
lt_iff_le_and_ne in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
lt_irrefl in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_add in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_fromNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_lt in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_mul in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toInt_one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
modularInterpret_step in IndisputableMonolith.Foundation.ModularLogicRealization decl_use
natOrderedRealization in IndisputableMonolith.Foundation.OrderedLogicRealization decl_use
modularRealization in IndisputableMonolith.Foundation.UniversalForcing.ModularRealization decl_use
orderRealization in IndisputableMonolith.Foundation.UniversalForcing.OrderRealization decl_use

Lean names referenced from this declaration's body.