46. Doubling gives an even number

EasyProofFree10 points

double n is n + n. Prove that it leaves remainder 0 when divided by 2, for every n.

The proof is two lines: one to look inside double, one to do the arithmetic.

Solution.lean

1def double (n : Nat) : Nat := n + n

2theorem solution (n : Nat) : double n % 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

⊢double n % 2 = 0

ReadyLn 1, Col 1Lean 4

Draft saved in this browser