2014-01-07 18:18:31 +00:00
|
|
|
|
Set: pp::colors
|
|
|
|
|
|
Set: pp::unicode
|
|
|
|
|
|
Imported 'macros'
|
|
|
|
|
|
Using: Nat
|
|
|
|
|
|
Assumed: Induction
|
|
|
|
|
|
Proved: Comm1
|
|
|
|
|
|
Proved: Comm2
|
|
|
|
|
|
theorem Comm2 : ∀ n m : ℕ, n + m = m + n :=
|
2014-01-08 08:38:39 +00:00
|
|
|
|
λ n : ℕ,
|
|
|
|
|
|
Induction
|
|
|
|
|
|
(λ x : ℕ, n + x == x + n)
|
|
|
|
|
|
(Nat::add::zeror n ⋈ symm (Nat::add::zerol n))
|
|
|
|
|
|
(λ (m : ℕ) (iH : n + m = m + n),
|
|
|
|
|
|
Nat::add::succr n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succl m n))
|
