∀ n : ℕ, P n → P (n + 1)
theorem ∘ proof ∘ verification
λ x. f (g x)
#check #eval #reduce
∃ k, n = 2 * k
by induction n with
Lua’s Webplace
ergodic theory, formalization, 🐈⬛s.