simp [not_lt.mpr le]
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ (‖S‖ ≤ i * ‖L‖ → 0 = 0) ∧
    (i * ‖L‖ < ‖S‖ →
      ∃ b ≤ S,
        Exponential (i * ‖L‖) b ∧ ∃ hL ≤ 2 * L + 1, Exponential ‖L‖ hL ∧ ∃ divS ≤ S, divS = S / b ∧ 0 = divS % hL)
no goals