theorem weak_duality {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