{α : ℕ → ℕ → Type} →
  {motive : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α → Sort u} →
    ((getElem : {n m : ℕ} → α n m → ℕ → ℕ → ℚ) →
        (setElem : {n m : ℕ} → α n m → ℕ → ℕ → ℚ → α n m) →
          (getValues : {n m : ℕ} → α n m → List (ℕ × ℕ × ℚ)) →
            (ofValues : {n m : ℕ} → List (ℕ × ℕ × ℚ) → α n m) →
              (swapRows : {n m : ℕ} → α n m → ℕ → ℕ → α n m) →
                (subtractRow : {n m : ℕ} → α n m → ℕ → ℕ → ℚ → α n m) →
                  (divideRow : {n m : ℕ} → α n m → ℕ → ℚ → α n m) →
                    motive
                      { getElem := getElem, setElem := setElem, getValues := getValues, ofValues := ofValues,
                        swapRows := swapRows, subtractRow := subtractRow, divideRow := divideRow }) →
      (t : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α) → motive t