-- The only solution to xᵃ = yᵇ + 1 with x,y,a,b > 1 is 3² = 2³ + 1. theorem catalan (x y a b : ℕ) (hx : 1 < x) (hy : 1 < y) (ha : 1 < a) (hb : 1 < b) (h : x ^ a = y ^ b + 1) : x = 3 ∧ a = 2 ∧ y = 2 ∧ b = 3 :=