theorem weak_duality_standard {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c x : Fin n → ℝ) (y : Fin m → ℝ) (hAx : A.mulVec x = b) (hx : ∀ (j : Fin n), 0 ≤ x j) (hATy : ∀ (j : Fin n), c j ≤ A.transpose.mulVec y j) : c ⬝ᵥ x ≤ b ⬝ᵥ y