equal
deleted
inserted
replaced
1830 assumes "n < m" |
1830 assumes "n < m" |
1831 shows "Suc (m - Suc n) = m - n" |
1831 shows "Suc (m - Suc n) = m - n" |
1832 proof - |
1832 proof - |
1833 from assms obtain q where "m = n + Suc q" |
1833 from assms obtain q where "m = n + Suc q" |
1834 by (auto dest: less_imp_Suc_add) |
1834 by (auto dest: less_imp_Suc_add) |
1835 moreover def r \<equiv> "Suc q" |
1835 moreover define r where "r = Suc q" |
1836 ultimately have "Suc (m - Suc n) = r" and "m = n + r" |
1836 ultimately have "Suc (m - Suc n) = r" and "m = n + r" |
1837 by simp_all |
1837 by simp_all |
1838 then show ?thesis by simp |
1838 then show ?thesis by simp |
1839 qed |
1839 qed |
1840 |
1840 |