theorem complementary_slackness {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c x : Fin n → ℝ) (y : Fin m → ℝ) (hAx : A.mulVec x ≤ b) (hx : 0 ≤ x) (hATy : A.transpose.mulVec y ≥ c) (hy : 0 ≤ y) : c ⬝ᵥ x = b ⬝ᵥ y ↔ (∀ (i : Fin m), (b i - A.mulVec x i) * y i = 0) ∧ ∀ (j : Fin n), (A.transpose.mulVec y j - c j) * x j = 0