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