`toNat_le`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.ArithmeticFromLogic on GitHub at line 452.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 449
 450/-! ## Recovery (Order): Peano order matches `Nat` order. -/
 451
 452theorem toNat_le (a b : LogicNat) : a ≤ b ↔ toNat a ≤ toNat b := by
 453  constructor
 454  · rintro ⟨k, hk⟩
 455    have := congrArg toNat hk
 456    rw [toNat_add] at this
 457    omega
 458  · intro h
 459    refine ⟨fromNat (toNat b - toNat a), ?_⟩
 460    have hroundtrip : ∀ n : LogicNat, fromNat (toNat n) = n := fromNat_toNat
 461    -- toNat (a + fromNat (toNat b - toNat a)) = toNat a + (toNat b - toNat a) = toNat b
 462    have hadd : toNat (a + fromNat (toNat b - toNat a)) = toNat b := by
 463      rw [toNat_add, toNat_fromNat]
 464      omega
 465    -- Apply equivNat injectivity
 466    have : a + fromNat (toNat b - toNat a) = b := by
 467      have h1 := congrArg fromNat hadd
 468      rw [hroundtrip, hroundtrip] at h1
 469      exact h1
 470    exact this
 471
 472theorem toNat_lt (a b : LogicNat) : a < b ↔ toNat a < toNat b := by
 473  rw [lt_iff_succ_le, toNat_le]
 474  constructor
 475  · intro h
 476    rw [toNat_succ] at h
 477    omega
 478  · intro h
 479    rw [toNat_succ]
 480    omega
 481
 482/-- `LogicNat` is a linear order: any two elements are comparable, and

papers checked against this theorem

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