2015-03-26 00:42:34 +00:00
|
|
|
import data.nat
|
2015-10-14 19:27:09 +00:00
|
|
|
open nat algebra
|
2015-03-26 00:42:34 +00:00
|
|
|
|
2015-07-07 23:37:06 +00:00
|
|
|
attribute nat.add [unfold 2]
|
|
|
|
|
attribute nat.rec_on [unfold 2]
|
2015-03-26 00:42:34 +00:00
|
|
|
|
|
|
|
|
example (a b c : nat) : a + 0 = 0 + a ∧ b + 0 = 0 + b :=
|
|
|
|
|
begin
|
|
|
|
|
apply and.intro,
|
|
|
|
|
all_goals (state; rewrite zero_add)
|
|
|
|
|
end
|
