def definition def or abbrev

`lt`

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

formal statement (Lean)

 328def lt (n m : LogicNat) : Prop := ∃ k : LogicNat, n + succ k = m

Definition body.

 329
 330instance : LE LogicNat := ⟨le⟩
 331instance : LT LogicNat := ⟨lt⟩
 332

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

le_antisymm in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
phi_neg58_lt in IndisputableMonolith.Numerics.Interval.PhiBounds decl_use
rung_gap_is_seven_halves in IndisputableMonolith.Physics.NeutrinoSector decl_use

Lean names referenced from this declaration's body.