axiom associativity_of_multiplication
    suppose a : Nat
    suppose b : Nat
    suppose c : Nat
    conclude eq(mult(mult(a, b), c), mult(a, mult(b, c)))

axiom idempotence_of_one
    suppose a : Nat
    conclude eq(mult(1, a), a)

axiom distributive_property_of_multiplication_over_addition
    suppose a : Nat
    suppose b : Nat
    suppose c : Nat
    conclude eq(mult(add(a, b), c), add(mult(a, c), mult(b, c)))

axiom associativity_of_addition
    suppose a : Nat
    suppose b : Nat
    suppose c : Nat
    conclude eq(add(add(a, b), c), add(a, add(b, c)))

axiom arithmetic1
    conclude eq(add(1, 1), 2)

# If a and b are propositions, and a and b are both true,
# then a and b is true.
theorem test1
    suppose a : Prop
    suppose b : Prop
    suppose h1 : a
    suppose h2 : b
    conclude and(a, b)
    proof
        unpack-and
            goal a
                proof
                    exact h1
            goal b
                proof
                    exact h2

# If a and b are propositions, and a and b are both true,
# then a and b and a is true.
theorem test2
    suppose a : Prop
    suppose b : Prop
    suppose h1 : a
    suppose h2 : b
    conclude and(a, and(b, a))
    proof
        unpack-and
            goal a
                proof
                    exact h1
            goal and(b, a)
                proof
                    unpack-and
                        goal b
                            proof
                                exact h2
                        goal a
                            proof
                                exact h1

# If a and (b or c) are true,
# then (a and b) or (a and c) is true.
theorem test3
    suppose a : Prop
    suppose b : Prop
    suppose c : Prop
    suppose h : and(a, or(b, c))
    conclude or(and(a, b), and(a, c))
    proof
        we-have or_b_c : or(b, c)
            proof
                exact right(h)
        cases or_b_c
            case h_b : b
                proof
                    assert-goal or(and(a, b), and(a, c))
                    focus-or left
                    assert-goal and(a, b)
                    unpack-and
                        goal a
                            proof
                                exact left(h)
                        goal b
                            proof
                                exact h_b
            case h_c : c
                proof
                    assert-goal or(and(a, b), and(a, c))
                    focus-or right
                    assert-goal and(a, c)
                    unpack-and
                        goal a
                            proof
                                exact left(h)
                        goal c
                            proof
                                exact h_c

# If there exists a natural number n such that P n is true,
# then there exists a natural number a such that P a is true.
theorem existence
    suppose P : func(Nat, Prop)
    suppose n : Nat
    suppose h : apply(P, n)
    conclude  exists(a : Nat, apply(P, a))
    proof
        witness n
        assert-goal apply(P, n)
        exact h

# If n is an even natural number,
# then n + 2 is also an even natural number.
theorem abc
    suppose n : Nat
    suppose h : exists(m : Nat, eq(n, mult(m, 2)))
    conclude exists(q : Nat, eq(add(n, 2), mult(q, 2)))
    proof
        deconstruct-exists h m h_m
        assert h_m : eq(n, mult(m, 2))
        define d_q : eq(q, add(m, 1))
        witness q
        assert-goal eq(add(n, 2), mult(q, 2))
        calculate add(n, 2)
            = add(mult(m, 2), 2) by-lhs h_m
            = add(mult(m, 2), mult(1, 2)) by-rhs idempotence_of_one 2
            = mult(add(m, 1), 2) by-rhs distributive_property_of_multiplication_over_addition m 1 2
            = mult(q, 2) by-rhs d_q

# If for every natural number n there exists a natural number m such that m = n + 1,
# then for every natural number t there exists a natural number u such that u = t + 2.    
theorem forall2
    suppose h : forall(n : Nat, exists(s : Nat, eq(s, add(n, 1))))
    conclude forall(t : Nat, exists(u : Nat, eq(u, add(t, 2))))
    proof
        consider t
        assert-goal exists(u : Nat, eq(u, add(t, 2)))
        forall-apply h t h2
        assert h2 : exists(s : Nat, eq(s, add(t, 1)))
        deconstruct-exists h2 m h_m
        assert h_m : eq(m, add(t, 1))
        forall-apply h m h3
        assert h3 : exists(s : Nat, eq(s, add(m, 1)))
        deconstruct-exists h3 u h_u
        assert h_u: eq(u, add(m, 1))
        witness u
        assert-goal eq(u, add(t, 2))
        calculate u
            = add(m, 1) by-lhs h_u
            = add(add(t, 1), 1) by-lhs h_m
            = add(t, add(1, 1)) by-lhs associativity_of_addition t 1 1
            = add(t, 2) by-lhs arithmetic1

# If m divides n and n divides p, then m divides p.
theorem divides_transitive
    suppose m : Nat
    suppose n : Nat
    suppose p : Nat
    suppose h1 : exists(k1 : Nat, eq(n, mult(m, k1)))
    suppose h2 : exists(k2 : Nat, eq(p, mult(n, k2)))
    conclude exists(k3 : Nat, eq(p, mult(m, k3)))
    proof
        deconstruct-exists h1 k1 h_n
        assert h_n : eq(n, mult(m, k1))
        deconstruct-exists h2 k2 h_p
        assert h_p : eq(p, mult(n, k2))
        define d_k3 : eq(k3, mult(k1, k2))
        witness k3
        assert-goal eq(p, mult(m, k3))
        calculate p
            = mult(n, k2) by-lhs h_p
            = mult(mult(m, k1), k2) by-lhs h_n
            = mult(m, mult(k1, k2)) by-lhs associativity_of_multiplication m k1 k2
            = mult(m, k3) by-rhs d_k3