case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_ne : n ≠ m
h : n ≤ m
⊢ IsMax ((succ^[n]) a)

case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax ((succ^[n]) a)
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_ne : n ≠ m
⊢ IsMax ((succ^[n]) a)
cases' le_total n m with h h
no goals
case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_ne : n ≠ m
h : n ≤ m
⊢ IsMax ((succ^[n]) a)
exact isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax ((succ^[m]) a)
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax ((succ^[n]) a)
rw [h_eq]
no goals
case inr
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
n m : ℕ
h_eq : (succ^[n]) a = (succ^[m]) a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax ((succ^[m]) a)
exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)