Gs num Vars gt num Constraints of gt one

lemma gs_numVars_gt_numConstraints_of_gt_one (hn : n ≠ 0) (hk : 1 < k) (hm : 1 ≤ m) :    numVars k (gs_degree_bound k n m) > numConstraints n m := by  set D := gs_degree_bound k n m  have hD : ((D + 1)^2 : ℝ) > ((m : ℝ) + 1 / 2)^2 * k * n := by    convert gs_degree_bound_sq_gt hn (by omega : 0 < k) using 1  have h_ineq : 2 * (k - 1) * numVars k D > (k - 1) * n * m * (m + 1) := by    have h_ineq : 2 * (k - 1) * numVars k D ≥ (D : ℝ) * (D + 2) := by      convert numVars_lower_bound_tight hk using 1      · norm_cast        rw [Int.subNatNat_of_le] <;> norm_cast        linarith    have h_ineq : (D : ℝ) * (D + 2) > (k - 1) * n * m * (m + 1) := by      nlinarith [show (k : ℝ) ≥ 2 by norm_cast, show (m : ℝ) ≥ 1 by        exact Nat.one_le_cast.mpr hm, show (n : ℝ) ≥ 1 by          exact Nat.one_le_cast.mpr (Nat.pos_of_ne_zero hn), mul_le_mul_of_nonneg_left            (show (m : ℝ) ≥ 1 by exact Nat.one_le_cast.mpr hm)              (show (n : ℝ) ≥ 0 by positivity)]    norm_cast at *    rw [Int.subNatNat_of_le] at * <;> (norm_cast at *; linarith)  have h_div : numVars k D > n * m * (m + 1) / 2 := by    exact Nat.div_lt_of_lt_mul <| by nlinarith [Nat.sub_pos_of_lt hk]  convert h_div using 1  convert congr_arg (fun x : ℕ ↦ n * x) (card_constraintIndices m) using 1  · rfl  · rw [← Nat.mul_div_assoc] <;> ring_nf    exact even_iff_two_dvd.mp (by simp [parity_simps])