K choose 2

@[simp]lemma k_choose_2 [Zero F] (h_n : n ≠ 0) :    n * choose_2 (k B) ≤ ∑ i, choose_2 (K B i 0) := by  suffices choose_2 (∑ i, (fun _ ↦ (1 : ℚ) / n) i • (fun i ↦ K B i 0) i) * n ≤      ∑ i, choose_2 (K B i 0) by    rw [mul_comm]; convert this; simp [k, mul_sum]  simp only [one_div, smul_eq_mul]  have hn_pos : (0 : ℚ) < n := by exact_mod_cast Nat.pos_of_ne_zero h_n  have jensen := ConvexOn.map_sum_le choose_2_convex    (t := univ (α := Fin n)) (w := fun _ ↦ (n : ℚ)⁻¹) (p := fun i ↦ (K B i 0 : ℚ))    (fun _ _ ↦ inv_nonneg.mpr hn_pos.le) (by simp; field_simp) (by simp)  simp only [smul_eq_mul] at jensen  exact le_trans (mul_le_mul_of_nonneg_right jensen hn_pos.le)    (le_of_eq (by rw [sum_mul]; congr 1; ext x; field_simp))