theorem proved term proof

`zero_ne_succ`

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

formal statement (Lean)

  89theorem zero_ne_succ (n : LogicNat) : zero ≠ succ n := by

proof body

Term-mode proof.

  90  intro h; cases h
  91
  92/-- **Peano P1, contrapositive**: every successor differs from zero. -/

used by (19)

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

canonicalCategoricalRealization in IndisputableMonolith.Foundation.CategoricalLogicRealization decl_use
logicNatNNO in IndisputableMonolith.Foundation.CategoricalLogicRealization decl_use
boolRealization in IndisputableMonolith.Foundation.DiscreteLogicRealization decl_use
ofPositiveRatioComparison in IndisputableMonolith.Foundation.LogicRealization decl_use
positiveRatio_faithful in IndisputableMonolith.Foundation.LogicRealization decl_use
modularRealization in IndisputableMonolith.Foundation.ModularLogicRealization decl_use
natOrderedRealization in IndisputableMonolith.Foundation.OrderedLogicRealization decl_use
physics_faithful in IndisputableMonolith.Foundation.PhysicsLogicRealization decl_use
physicsRealization in IndisputableMonolith.Foundation.PhysicsLogicRealization decl_use
biologyRealization in IndisputableMonolith.Foundation.UniversalForcing.BiologyRealization decl_use
ethicsRealization in IndisputableMonolith.Foundation.UniversalForcing.EthicsRealization decl_use
modularRealization in IndisputableMonolith.Foundation.UniversalForcing.ModularRealization decl_use
musicRealization in IndisputableMonolith.Foundation.UniversalForcing.MusicRealization decl_use
narrativeRealization in IndisputableMonolith.Foundation.UniversalForcing.NarrativeRealization decl_use
interpret_collapses in IndisputableMonolith.Foundation.UniversalForcing.NaturalNumberObject decl_use
orderRealization in IndisputableMonolith.Foundation.UniversalForcing.OrderRealization decl_use
strictCategoricalRealization in IndisputableMonolith.Foundation.UniversalForcing.Strict.Categorical decl_use
toLightweight in IndisputableMonolith.Foundation.UniversalForcing.StrictRealization decl_use
logicRealizationOfDistinction in IndisputableMonolith.Foundation.UniversalInstantiationFromDistinction decl_use

depends on (4)

Lean names referenced from this declaration's body.

LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
succ in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
succ in IndisputableMonolith.RRF.Core.Vantage decl_use