equal
deleted
inserted
replaced
171 apply(simp del: diff_is_0_eq) |
171 apply(simp del: diff_is_0_eq) |
172 apply(subgoal_tac "Suc nata\<le>nat") |
172 apply(subgoal_tac "Suc nata\<le>nat") |
173 prefer 2 apply arith |
173 prefer 2 apply arith |
174 apply(drule_tac n = "Suc nata" in Compl_lemma) |
174 apply(drule_tac n = "Suc nata" in Compl_lemma) |
175 apply clarify |
175 apply clarify |
176 using [[option fast_arith_split_limit = 0]] |
176 using [[fast_arith_split_limit = 0]] |
177 apply force |
177 apply force |
178 using [[option fast_arith_split_limit = 9]] |
178 using [[fast_arith_split_limit = 9]] |
179 apply(drule leI) |
179 apply(drule leI) |
180 apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)") |
180 apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)") |
181 apply(erule_tac x = "m - (Suc nata)" in allE) |
181 apply(erule_tac x = "m - (Suc nata)" in allE) |
182 apply(case_tac "m") |
182 apply(case_tac "m") |
183 apply simp |
183 apply simp |