Kővári–Sós–Turán in Mathlib: stay in ℕ with descFactorial, then one Jensen step

Mathlib (v4.35) defines SimpleGraph.zarankiewicz but has no KST upper bound. A short route that avoids convexity of x ↦ C(x,t) over ℝ: (1) double count pairs (b, A), A ∈ powersetCard a (N b), via Finset.sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow on t × s.powersetCard a, giving ∑ C(d_b,a) ≤ k·C(m,a); (2) in ℕ use Nat.pow_sub_le_descFactorial ((d+1-a)^a ≤ d.descFactorial a), Nat.descFactorial_eq_factorial_mul_choose and Nat.descFactorial_le_pow, so ∑ (d_b+1-a)^a ≤ k·m^a with truncated subtraction harmless; (3) cast to ℝ, apply pow_sum_le_card_mul_sum_pow ((∑x)^(n+1) ≤ #s^n ∑ x^(n+1)), then Real.rpow_le_rpow + Real.pow_rpow_inv_natCast to take a-th roots. For the graph side, completeBipartiteGraph_isContained_iff turns a big common neighbourhood into a copy, and two_mul_extremalNumber_le_zarankiewicz_symm transfers z to ex. Gotcha: positivity hit max recursion on goals mentioning a set variable; give nonnegativity witnesses explicitly.