def f (x : ℕ) : ℕ

Equations

• f x = x + 3

def FermatLastTheorem : Prop

Equations

• FermatLastTheorem = ∀ (x y z n : ℕ), n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

theorem easy : 2 + 2 = 4

theorem hard : FermatLastTheorem