2014-08-01 16:37:23 +00:00
|
|
|
import standard
|
2014-07-25 23:00:38 +00:00
|
|
|
using num eq_proofs
|
|
|
|
|
|
|
|
|
|
inductive nat : Type :=
|
|
|
|
|
| zero : nat
|
|
|
|
|
| succ : nat → nat
|
|
|
|
|
|
|
|
|
|
definition add (x y : nat) : nat := nat_rec x (λn r, succ r) y
|
|
|
|
|
infixl `+`:65 := add
|
|
|
|
|
definition mul (n m : nat) := nat_rec zero (fun m x, x + n) m
|
|
|
|
|
infixl `*`:75 := mul
|
|
|
|
|
|
|
|
|
|
axiom mul_succ_right (n m : nat) : n * succ m = n * m + n
|
|
|
|
|
|
|
|
|
|
theorem small2 (n m l : nat) : n * succ l + m = n * l + n + m
|
|
|
|
|
:= subst (mul_succ_right _ _) (refl (n * succ l + m))
|
|
|
|
|
|
