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

lt_iff_succ_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)

 356theorem lt_iff_succ_le {n m : LogicNat} : n < m ↔ succ n ≤ m := by

proof body

Term-mode proof.

 357  constructor
 358  · rintro ⟨k, hk⟩
 359    refine ⟨k, ?_⟩
 360    show succ n + k = m
 361    rw [succ_add]
 362    show succ (n + k) = m
 363    rw [← add_succ]
 364    -- need n + succ k = m, but we have n + succ k = m via hk; succ_add transforms
 365    -- Wait: hk : n + succ k = m, and succ (n + k) = n + succ k by add_succ. So succ (n + k) = m.
 366    exact hk
 367  · rintro ⟨k, hk⟩
 368    refine ⟨k, ?_⟩
 369    show n + succ k = m
 370    rw [add_succ]
 371    show succ (n + k) = m
 372    rw [← succ_add]
 373    exact hk
 374

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.