rw [←sub_sub, sub_add_self_of_le]
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
this : P (a - x)
⊢ P (a - (x + 1) + 1)
M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
this : P (a - x)
⊢ P (a - x)

M : Type u_1
inst✝¹⁰ : Zero M
inst✝⁹ : One M
inst✝⁸ : Add M
inst✝⁷ : Mul M
inst✝⁶ : LT M
inst✝⁵ : M ⊧ₘ* 𝐏𝐀⁻
L : Language
inst✝⁴ : L.ORing
inst✝³ : Structure L M
inst✝² : Structure.ORing L M
inst✝¹ : Structure.Monotone L M
Γ : Polarity
m : ℕ
inst✝ : M ⊧ₘ* Theory.indScheme L (Hierarchy Γ m)
P : M → Prop
hP : DefinablePred L (Γ.coe, m) P
nzero : ¬P 0
nsucc : ∀ (x : M), ¬P x → ¬P (x + 1)
A : ¬∀ (x : M), ¬P x
a : M
ha : P a
x : M
IH : x ≤ a → P (a - x)
hx : x + 1 ≤ a
this : P (a - x)
⊢ 1 ≤ a - x