| changeset 47193 | 9ae03b37b4f6 |
| parent 47192 | 0c0501cb6da6 |
| child 47194 | 6e53f2a718c2 |
| 47192:0c0501cb6da6 | 47193:9ae03b37b4f6 |
|---|---|
36 apply (simp add: nat_eq_iff) |
36 apply (simp add: nat_eq_iff) |
37 done |
37 done |
38 |
38 |
39 lemma Suc_nat_number_of_add: |
39 lemma Suc_nat_number_of_add: |
40 "Suc (numeral v + n) = numeral (v + Num.One) + n" |
40 "Suc (numeral v + n) = numeral (v + Num.One) + n" |
41 by simp |
|
42 |
|
43 lemma Suc_numeral [simp]: |
|
44 "Suc (numeral v) = numeral (v + Num.One)" |
|
45 by simp |
41 by simp |
46 |
42 |
47 |
43 |
48 subsubsection{*Subtraction *} |
44 subsubsection{*Subtraction *} |
49 |
45 |