List of theorems

List of theorems in general/Basic_arithmetic_implies_Peano_axioms.gh:

(= (succ a) (+ a (1)))

(↔ (= (succ a) (succ b)) (= a b))

(= (+ a (0)) a)

(= (+ a (succ b)) (succ (+ a b)))

(= (· a (0)) (0))

(= (· a (succ b)) (+ a (· a b)))

(→ (∧ (subst (0) n φ) (∀ k (→ (subst k n φ) (subst (succ k) n φ)))) (∀ n φ))

(¬ (= (0) (succ a)))