lemma[simp]: "mul (Suc n) m = m + n * m"
  apply (induction m)
   apply auto
  done

lemma "mul n m = n * m"
  apply (induction n)
   apply auto
  done

fun sub :: "nat ⇒ nat ⇒ nat"
  where 
    "sub 0 m = 0" |
    "sub n 0 = n" |
    "sub (Suc n) (Suc m) = sub n m"

lemma[simp]: "sub 0 m ≡ 0"
  by simp

lemma[simp]: "sub n 0 = n"
  apply (induction n)
   apply auto
  done

lemma[simp]: "sub m m = 0"
  apply (induction m)
   apply auto
  done

lemma[simp]: "sub n (Suc 0) = n - Suc 0"
  apply (induction n)
   apply auto
  done

sub n m = 0

m >= n

sub n m = n - m

m < n