Polynomial induction

@[elab_as_elim]lemma polynomial_induction [V↓[ℒₒᵣ] ⊧* 𝗣𝗔⁻] (Γ m) [V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ m]    {P : V → Prop} (hP : Γ-[m]-Predicate P)    (zero : P 0) (even : ∀ x > 0, P x → P (2 * x)) (odd : ∀ x, P x → P (2 * x + 1)) : ∀ x, P x := by  have : V↓[ℒₒᵣ] ⊧* 𝗜𝗡𝗗 Γ m := inferInstance  have : V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻 := models_of_subtheory this  intro x; induction x using InductionOnHierarchy.order_induction  · exact Γ  · exact m  · exact hP  case inst => exact inferInstance  case ind x IH =>    rcases Arithmetic.zero_le x with (rfl | pos)    · exact zero    · have : x / 2 < x := div_lt_of_pos_of_one_lt pos one_lt_two      rcases even_or_odd' x with (hx | hx)      · simpa [←hx] using even (x / 2) (by by_contra A; simp at A; simp [show x = 0 from by simpa [A] using hx] at pos) (IH (x / 2) this)      · simpa [←hx] using odd (x / 2) (IH (x / 2) this)