noncomputable def sdAugMat {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (c : Fin n → ℝ) : Matrix (Fin (m + 1)) (Fin (n + 1)) ℝ

noncomputable def sdAugRhs {m : ℕ} (b : Fin m → ℝ) (v : ℝ) : Fin (m + 1) → ℝ

theorem augSys_to_primal {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (c : Fin n → ℝ) (b : Fin m → ℝ) (v : ℝ) (z : Fin (n + 1) → ℝ) (hz_nn : ∀ (j : Fin (n + 1)), 0 ≤ z j) (hBz : (sdAugMat A c).mulVec z = sdAugRhs b v) : have x := fun (j : Fin n) => z j.castSucc; (∀ (j : Fin n), 0 ≤ x j) ∧ A.mulVec x = b ∧ c ⬝ᵥ x ≥ v

theorem sd_farkas_alternative_false {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c x₀ : Fin n → ℝ) (hx₀_nn : ∀ (j : Fin n), 0 ≤ x₀ j) (hAx₀ : A.mulVec x₀ = b) (v : ℝ) (hv_ub : ∀ (y : Fin m → ℝ), (∀ (j : Fin n), c j ≤ A.transpose.mulVec y j) → v ≤ b ⬝ᵥ y) (w : Fin (m + 1) → ℝ) (hw_nn : ∀ (j : Fin (n + 1)), 0 ≤ (sdAugMat A c).transpose.mulVec w j) (hw_dot : sdAugRhs b v ⬝ᵥ w < 0) : False

noncomputable def dualAugMat {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) : Matrix (Fin (n + 1)) (Fin (m + (m + (n + 1)))) ℝ

noncomputable def dualAugRhs {n : ℕ} (c : Fin n → ℝ) (v : ℝ) : Fin (n + 1) → ℝ

theorem augDualSys_to_dual {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c : Fin n → ℝ) (v : ℝ) (z : Fin (m + (m + (n + 1))) → ℝ) (hz_nn : ∀ (k : Fin (m + (m + (n + 1)))), 0 ≤ z k) (hCz : (dualAugMat A b).mulVec z = dualAugRhs c v) : have y_opt := fun (i : Fin m) => z (Fin.castAdd (m + (n + 1)) i) - z (Fin.natAdd m (Fin.castAdd (n + 1) i)); (∀ (j : Fin n), c j ≤ A.transpose.mulVec y_opt j) ∧ b ⬝ᵥ y_opt ≤ v

theorem sd_dual_farkas_alternative_false {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (c : Fin n → ℝ) (v : ℝ) (hv_is_ub : ∀ (x : Fin n → ℝ), (∀ (j : Fin n), 0 ≤ x j) → A.mulVec x = b → c ⬝ᵥ x ≤ v) (x₀ : Fin n → ℝ) (hx₀_nn : ∀ (j : Fin n), 0 ≤ x₀ j) (hAx₀ : A.mulVec x₀ = b) (w : Fin (n + 1) → ℝ) (hw_nn : ∀ (k : Fin (m + (m + (n + 1)))), 0 ≤ (dualAugMat A b).transpose.mulVec w k) (hw_dot : dualAugRhs c v ⬝ᵥ w < 0) : False

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