| changeset 14738 | 83f1a514dcb4 |
| parent 14723 | b77ce15b625a |
| child 15481 | fc075ae929e4 |
| 14737:77ea79aed99d | 14738:83f1a514dcb4 |
|---|---|
20 apply (induct_tac d) |
20 apply (induct_tac d) |
21 apply (induct_tac m) |
21 apply (induct_tac m) |
22 apply (simp) |
22 apply (simp) |
23 apply (force) |
23 apply (force) |
24 apply (simp) |
24 apply (simp) |
25 apply (subst plus_ac0.commute[of m]) |
25 apply (subst ab_semigroup_add.add_commute[of m]) |
26 apply (simp) |
26 apply (simp) |
27 done |
27 done |
28 |
28 |
29 end |
29 end |
30 |
30 |