David Tran’s blog

fac1 :: Integer -> Integer
fac1 0 = 1
fac1 n = n * fac1 (n - 1)

fac2 :: Integer -> Integer
fac2 n = fac' n 1
  where fac' 0 x = x
        fac' n x = fac' (n - 1) (n * x)

Prove that fac1 n = fac2 n for all nonnegative integers n.

(a) base step: n = 0
fac1 0 = 1
fac2 0 = fac' 0 1 = 1
==> Proven.

(b) induction hypothesis: Assume that  fac1 n = fac2 n
fac1 (n+1)
= (n+1) * fac1 n
= (n+1) * fac2 n   -- due to induction hypothesis
= (n+1) * fac' n 1
= (n+1) * fac' (n-1) n
= (n+1) * fac' (n-2) (n * (n-1))
...
= (n+1) * n * (n-1) * (n-2) * ... * 1

fac2 (n+1)
= fac' (n+1) 1
= fac' n (n+1)
= fac' (n-1) ((n+1) * n)
...
= (n+1) * n * (n-1) * (n-2) * ... * 1

so, fac1 (n+1) = fac2 (n+1)
==> Proven.