open nat

--1.a.
example : ∀ m n k : nat, m * (n + k) = m * n + m * k :=
assume m n k,
nat.rec_on k
(show m * (n + 0) = m * n + m * 0, from calc
m * (n + 0) = m * n : by rw add_zero
        ... = m * n + 0 : by rw add_zero
        ... = m * n + m * 0 : by rw mul_zero)

(assume k,
assume ih: m * (n + k) = m * n + m * k,
show m * (n + succ k) = m * n + m * (succ k), from calc
m * (n + succ k) = m * (succ (n + k)) : by rw add_succ
             ... = m * (n + k) + m : by rw mul_succ
             ... = m * n + m * k + m : by rw ih
             ... = m * n + (m * k + m) : by simp
             ... = m * n + m * (succ k) : by rw mul_succ)


--1.b.
example : ∀ n : nat, 0 * n = 0 :=
assume n,
nat.rec_on n
(show 0 * 0 = 0, from dec_trivial)
(assume n,
assume ih : 0 * n = 0,
show 0 * (succ n) = 0, from calc
0 * (succ n) = 0 * n + 0 : by rw mul_succ
         ... = 0 * n : by rw add_zero
         ... = 0 : by rw ih)


--1.c.
example : ∀ n : nat, 1 * n = n :=
assume n,
nat.rec_on n
    (show 1 * 0 = 0, from dec_trivial)
    (assume n,
    assume ih : 1 * n = n,
    show 1 * (succ n) = succ n, from calc
    1 * (succ n) = 1 * n + 1 : by rw mul_succ
           ... = n + 1 : by rw ih
           ... = succ n : by simp)



--1.d.
example : ∀ m n k : nat, (m * n) * k = m * (n * k) := sorry

--1.e.
example : ∀ m n : nat, m * n= n * m := sorry