diff -r 6d96ee03b62e -r 4df0628e8545 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Jul 11 18:37:52 2019 +0200
+++ b/src/HOL/Parity.thy	Wed Jul 17 14:02:42 2019 +0100
@@ -574,6 +574,28 @@
   \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close>
   using that by auto
 
+lemma nat_induct2 [case_names 0 1 step]:
+  assumes "P 0" "P 1" and step: "\<And>n::nat. P n \<Longrightarrow> P (n + 2)"
+  shows "P n"
+proof (induct n rule: less_induct)
+  case (less n)
+  show ?case
+  proof (cases "n < Suc (Suc 0)")
+    case True
+    then show ?thesis
+      using assms by (auto simp: less_Suc_eq)
+  next
+    case False
+    then obtain k where k: "n = Suc (Suc k)"
+      by (force simp: not_less nat_le_iff_add)
+    then have "k<n"
+      by simp
+    with less assms have "P (k+2)"
+      by blast
+    then show ?thesis
+      by (simp add: k)
+  qed
+qed
 
 subsection \<open>Parity and powers\<close>