Existence of basic feasible solutions for bounded and standard-form polyhedra

import Definitions.Def_Polyhedron
import Definitions.Def_BasicSolution


/-- **B&T Corollary 2.2 (p. 65).** Every nonempty bounded general-form
polyhedron, and every nonempty standard-form polyhedron, has at least one
basic feasible solution (with respect to its presentation). -/

theorem LinearOptimization.polyhedron_std_form_has_bfs {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) :
    ((polyhedron A b).Nonempty → IsBoundedSet (polyhedron A b) →
      ∃ x, IsBasicFeasibleSolution (generalFormSystem A b) x) ∧
    ((stdPolyhedron A b).Nonempty →
      ∃ x, IsBasicFeasibleSolution (stdFormSystem A b) x) := by
  sorry