equal
deleted
inserted
replaced
28 assume "r = b" |
28 assume "r = b" |
29 with I have "Suc a = Suc b * (Suc q) + 0 \<and> 0 \<le> b" by simp |
29 with I have "Suc a = Suc b * (Suc q) + 0 \<and> 0 \<le> b" by simp |
30 thus ?case by iprover |
30 thus ?case by iprover |
31 next |
31 next |
32 assume "r \<noteq> b" |
32 assume "r \<noteq> b" |
33 hence "r < b" by (simp add: order_less_le) |
33 with `r \<le> b` have "r < b" by (simp add: order_less_le) |
34 with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp |
34 with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp |
35 thus ?case by iprover |
35 thus ?case by iprover |
36 qed |
36 qed |
37 qed |
37 qed |
38 |
38 |