diff --git a/Mathlib/Data/Nat/EvenOddRec.lean b/Mathlib/Data/Nat/EvenOddRec.lean
index 34b38b9565055..085c3ed55f705 100644
--- a/Mathlib/Data/Nat/EvenOddRec.lean
+++ b/Mathlib/Data/Nat/EvenOddRec.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Stuart Presnell. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stuart Presnell
 -/
-import Mathlib.Init.Data.Nat.Bitwise
+import Mathlib.Data.Nat.Parity
 
 #align_import data.nat.even_odd_rec from "leanprover-community/mathlib"@"18a5306c091183ac90884daa9373fa3b178e8607"
 /-! # A recursion principle based on even and odd numbers. -/
@@ -18,7 +18,6 @@ namespace Nat
 extend from `P i` to both `P (2 * i)` and `P (2 * i + 1)`, then we have `P n` for all `n : ℕ`.
 This is nothing more than a wrapper around `Nat.binaryRec`, to avoid having to switch to
 dealing with `bit0` and `bit1`. -/
-
 @[elab_as_elim]
 def evenOddRec {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ n, P n → P (2 * n))
     (h_odd : ∀ n, P n → P (2 * n + 1)) (n : ℕ) : P n :=
@@ -36,7 +35,7 @@ theorem evenOddRec_zero (P : ℕ → Sort*) (h0 : P 0) (h_even : ∀ i, P i →
 @[simp]
 theorem evenOddRec_even (n : ℕ) (P : ℕ → Sort*) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
     (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
-    @evenOddRec _ h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n) :=
+    (2 * n).evenOddRec h0 h_even h_odd = h_even n (evenOddRec h0 h_even h_odd n) :=
   have : ∀ a, bit false n = a →
       HEq (@evenOddRec _ h0 h_even h_odd a) (h_even n (evenOddRec h0 h_even h_odd n))
     | _, rfl => by rw [evenOddRec, binaryRec_eq]; apply eq_rec_heq; exact H
@@ -46,11 +45,22 @@ theorem evenOddRec_even (n : ℕ) (P : ℕ → Sort*) (h0 : P 0) (h_even : ∀ i
 @[simp]
 theorem evenOddRec_odd (n : ℕ) (P : ℕ → Sort*) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
     (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
-    @evenOddRec _ h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n) :=
+    (2 * n + 1).evenOddRec h0 h_even h_odd = h_odd n (evenOddRec h0 h_even h_odd n) :=
   have : ∀ a, bit true n = a →
       HEq (@evenOddRec _ h0 h_even h_odd a) (h_odd n (evenOddRec h0 h_even h_odd n))
     | _, rfl => by rw [evenOddRec, binaryRec_eq]; apply eq_rec_heq; exact H
   eq_of_heq (this _ (bit1_val _))
 #align nat.even_odd_rec_odd Nat.evenOddRec_odd
 
+/-- Strong recursion principle on even and odd numbers: if for all `i : ℕ` we can prove `P (2 * i)`
+from `P j` for all `j < 2 * i` and we can prove `P (2 * i + 1)` from `P j` for all `j < 2 * i + 1`,
+then we have `P n` for all `n : ℕ`. -/
+@[elab_as_elim]
+noncomputable def evenOddStrongRec {P : ℕ → Sort*} (n : ℕ)
+    (h_even : ∀ n : ℕ, (∀ k < 2 * n, P k) → P (2 * n))
+    (h_odd : ∀ n : ℕ, (∀ k < 2 * n + 1, P k) → P (2 * n + 1)) : P n :=
+  n.strongRecOn fun m ih => m.even_or_odd'.choose_spec.by_cases
+    (fun h => h.symm ▸ h_even m.even_or_odd'.choose <| h ▸ ih)
+    (fun h => h.symm ▸ h_odd m.even_or_odd'.choose <| h ▸ ih)
+
 end Nat