Num Vars lower bound tight

lemma numVars_lower_bound_tight {D : ℕ} (hk : 1 < k) :    2 * (k - 1) * numVars k D ≥ D * (D + 2) := by      have h_numVars_def : numVars k D =          ((D / (k - 1)) + 1) * (2 * D + 2 - (k - 1) * (D / (k - 1))) / 2 :=        numVars_eq_of_gt_one hk      rcases k with (_|_|k) <;> simp_all only [lt_add_iff_pos_left, add_pos_iff, zero_lt_one,        or_true, add_tsub_cancel_right, Nat.mul_succ, ge_iff_le]      · omega      · omega      rw [← Nat.mul_div_assoc]      · rw [Nat.le_div_iff_mul_le] <;> ring_nf        · zify          rw [Nat.cast_sub] <;> push_cast <;>            nlinarith [D.div_mul_le_self (1 + k), D.div_add_mod (1 + k),              D.mod_lt (by linarith : 0 < (1 + k))]        · norm_num      · cases le_total (2 * D + 2) ((k + 1) * (D / (k + 1))) <;>          simp_all [← even_iff_two_dvd, parity_simps]        by_cases h : Even (D / (k + 1)) <;> simp_all [parity_simps]