def fac : ℕ → ℕ

Equations

• fac 0 = 1
• fac n.succ = (n + 1) * fac n

theorem fac_pos (n : ℕ) : 0 < fac n

theorem dvd_fac {i : ℕ} {n : ℕ} (ipos : 0 < i) (ile : i ≤ n) : i ∣ fac n

theorem pow_two_le_fac (n : ℕ) : 2 ^ (n - 1) ≤ fac n

theorem sum_id (n : ℕ) : ∑ i ∈ Finset.range (n + 1), i = n * (n + 1) / 2

theorem sum_sqr (n : ℕ) : ∑ i ∈ Finset.range (n + 1), i ^ 2 = n * (n + 1) * (2 * n + 1) / 6

inductive MyNat : Type

• zero: MyNat
• succ: MyNat → MyNat

def MyNat.add : MyNat → MyNat → MyNat

Equations

• x.add MyNat.zero = x
• x.add y.succ = (x.add y).succ

def MyNat.mul : MyNat → MyNat → MyNat

Equations

• x.mul MyNat.zero = MyNat.zero
• x.mul y.succ = (x.mul y).add x

theorem MyNat.zero_add (n : MyNat) : MyNat.zero.add n = n

theorem MyNat.succ_add (m : MyNat) (n : MyNat) : m.succ.add n = (m.add n).succ

theorem MyNat.add_comm (m : MyNat) (n : MyNat) : m.add n = n.add m

theorem MyNat.add_assoc (m : MyNat) (n : MyNat) (k : MyNat) : (m.add n).add k = m.add (n.add k)

theorem MyNat.mul_add (m : MyNat) (n : MyNat) (k : MyNat) : m.mul (n.add k) = (m.mul n).add (m.mul k)

theorem MyNat.zero_mul (n : MyNat) : MyNat.zero.mul n = MyNat.zero

theorem MyNat.succ_mul (m : MyNat) (n : MyNat) : m.succ.mul n = (m.mul n).add n

theorem MyNat.mul_comm (m : MyNat) (n : MyNat) : m.mul n = n.mul m