`lt_trans`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.ArithmeticFromLogic
domain: Foundation
line: 383 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 383.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 380  -- this : toNat n + Nat.succ (toNat k) = toNat n
 381  omega
 382
 383theorem lt_trans {a b c : LogicNat} (hab : a < b) (hbc : b < c) : a < c := by
 384  rw [lt_iff_succ_le] at hab hbc ⊢
 385  exact le_trans hab (le_trans (le_succ b) hbc)
 386
 387theorem zero_lt_succ (n : LogicNat) : zero < succ n :=
 388  ⟨n, by show zero + succ n = succ n; rw [zero_add]⟩
 389
 390theorem lt_iff_le_and_ne {a b : LogicNat} : a < b ↔ a ≤ b ∧ a ≠ b := by
 391  constructor
 392  · rintro ⟨k, hk⟩
 393    refine ⟨⟨succ k, hk⟩, ?_⟩
 394    intro hab
 395    rw [hab] at hk
 396    -- b + succ k = b means succ k = 0 by additive cancellation; impossible.
 397    have := congrArg toNat hk
 398    rw [toNat_add, toNat_succ] at this
 399    omega
 400  · rintro ⟨⟨k, hk⟩, hne⟩
 401    -- a + k = b, a ≠ b, so k ≠ 0; k = succ k' for some k'.
 402    cases k with
 403    | identity =>
 404      exfalso
 405      apply hne
 406      simpa using hk
 407    | step k' => exact ⟨k', hk⟩
 408
 409theorem le_antisymm {a b : LogicNat} (hab : a ≤ b) (hba : b ≤ a) : a = b := by
 410  obtain ⟨k1, hk1⟩ := hab
 411  obtain ⟨k2, hk2⟩ := hba
 412  have h1 := congrArg toNat hk1
 413  have h2 := congrArg toNat hk2

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.