page 1 1

We want to prove
( M  N  : Nat  )
(2 * M) * M = N * N
implies
(K  : Nat  ) N = 2 * K .
We take the following steps:
• Quantifier elimination introduces the new constant(s) m, n : Nat  .
• Implication elimination assumes  (2 * m) * m = n * n .
• We introduce the lemma  ( M  : Nat  )        (N  : Nat  )                   M = 2 * N             or                   M = (2 * N) + 1.
• In the following hypothesis  ( M  : Nat  )        (N  : Nat  )                   M = 2 * N             or                   M = (2 * N) + 1 ,
let M  = n , we get  (N  : Nat  )             n = 2 * N       or             n = (2 * N) + 1 ,
• By skolemization, we can get  n = 2 * n1 or       n = (2 * n1) + 1
from the following hypothesis  (N  : Nat  )             n = 2 * N       or             n = (2 * N) + 1 .
• We do case analysis on  n = 2 * n1 or       n = (2 * n1) + 1 ,
and we get 2 cases:
1. Case: n = 2 * n1 .
• We change the equation n = 2 * n1 to rewriting rule.
• Let K = n1 . Then we need to prove  n = 2 * n1 .
• We show n = 2 * n1 by reduction.
2. Case: n = (2 * n1) + 1 .
• Then we apply equation n = (2 * n1) + 1 to the hypothesis  (2 * m) * m = n * n ,
and get  (2 * m) * m = s (((((n1 * n1) + (n1 * n1)) + ((n1 * n1) + (n1 * n1))) + (n1 + n1)) + (n1 + n1)) ,
• We introduce the lemma  ( M  : Nat  ) mod2(2 * M) = 0.