Theorem: Nat.one_le_succ (LeanMeetup/Exercise02Solutions.lean)

State before:
x : ℕ
⊢ 1 ≤ succ x
Tactic:
exact tsub_add_cancel_iff_le.mp rfl
State after:
no goals