theorem proved term proof

`le_succ`

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

formal statement (Lean)

 346theorem le_succ (n : LogicNat) : n ≤ succ n := ⟨succ zero, by

Term-mode proof.

 347  show n + succ zero = succ n
 348  rw [add_succ, add_zero]⟩
 349

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

ballP_subset_inBall in IndisputableMonolith.Causality.BallP decl_use
ballP_subset_inBall in IndisputableMonolith.Causality.Reach decl_use
circuitLedgerCert in IndisputableMonolith.Complexity.CircuitLedger decl_use
lt_trans in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
PossibilitySpace in IndisputableMonolith.Modal.Possibility decl_use
defect_cost_unbounded in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
exists_shift_ae_abs_sub_le_of_oscOn_Icc_exhaustion in IndisputableMonolith.NumberTheory.RiemannHypothesis.LocalToGlobalWedge decl_use

Lean names referenced from this declaration's body.