rcases show i * ‖L‖ < ‖S'‖ ∨ ‖S'‖ ≤ i * ‖L‖ from lt_or_ge (i * ‖L‖) ‖S'‖ with (lt' | le')
case inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0
case inr.inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
lt' : i * ‖L‖ < ‖S'‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0

case inr.inr
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
L S S' i : M
h : S ≤ S'
le : ‖S‖ ≤ i * ‖L‖
le' : ‖S'‖ ≤ i * ‖L‖
⊢ S / bexp S' (i * ‖L‖) % L # 1 = 0