∀ (n : ℕ),
  CartanMatrix.D n =
    Matrix.of fun i j =>
      if i = j then 2
      else
        if n ≤ 2 then 0
        else
          if ↑i + 1 = ↑j ∧ ↑j + 2 < n then -1
          else
            if ↑j + 1 = ↑i ∧ ↑i + 2 < n then -1
            else
              if ↑i + 3 = n ∧ (↑j + 2 = n ∨ ↑j + 1 = n) then -1
              else if ↑j + 3 = n ∧ (↑i + 2 = n ∨ ↑i + 1 = n) then -1 else 0