Every number is less than its successor

Exercise · lt_succ_self'

Every number is less than its successor: $n < n + 1$ .

Formal statement · Lean 4.lean

theorem lt_succ_self' (n : Nat) : n < n + 1 := by
  sorry

Proof. sorry

Nobody has tried yet.