have : exp i < exp j := calc
  exp i ≤ exp j - 1 := exp_le_of_mem h
  _     < exp j     := pred_lt_self_of_pos (exp_pos j)
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : i ∈ under j
⊢ i < j
case mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
i j : M
h : i ∈ under j
this : exp i < exp j
⊢ i < j