rw [ext_graph_aux]
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
⊢ z = S{L}[i] ↔
    ∃ 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)
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
⊢ (‖S‖ ≤ i * ‖L‖ → z = 0) ∧ (i * ‖L‖ < ‖S‖ → ∃ b ≤ S, Exponential (i * ‖L‖) b ∧ z = S / b % L # 1) ↔
    ∃ 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)