pith. machine review for the scientific record. sign in
theorem proved tactic proof

toNat_le

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 452theorem toNat_le (a b : LogicNat) : a ≤ b ↔ toNat a ≤ toNat b := by

proof body

Tactic-mode proof.

 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

used by (3)

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

depends on (8)

Lean names referenced from this declaration's body.