constructor
case inl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ z = 0 ↔
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)
case inl.mp
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
z S L i : M
le : ‖S‖ ≤ i * ‖L‖
⊢ z = 0 →
    ∃ lS ≤ S,
      lS = ‖S‖ ∧
        ∃ lL ≤ L,
          lL = ‖L‖ ∧
            (lS ≤ i * lL → z = 0) ∧
              (i * lL < lS →
                ∃ b ≤ S,
                  Exponential (i * lL) b ∧
                    ∃ hL ≤ 2 * L + 1, Exponential lL hL ∧ ∃ divS ≤ S, divS = S / b ∧ z = divS % hL)

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