10. An even number above n

EasyProofFree10 points

Prove that for every natural number n there is an even number m with n < m. You have to name the witness yourself.

Solution.lean

1theorem solution (n : Nat) : ∃ m, n < m ∧ m % 2 = 0 := by

given

Loading editor…

Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.

n:Nat

⊢∃ m, n < m ∧ m % 2 = 0

ReadyLn 1, Col 1Lean 4

Draft saved in this browser