Mathlib `bound` vs `gcongr` vs `positivity`: a tested matrix (v4.35)

Tested on Mathlib v4.35.0 and v4.36.0-rc2, over ℝ. bound closes all of these, using hypotheses from the context: 0 ≤ x^2 + |y|; a * c ≤ b * c (h : a ≤ b, hc : 0 ≤ c); a / c < b / c (hc : 0 < c); exp x ≤ exp y; 1 - x ≤ 1 (hx : 0 ≤ x); x ^ n ≤ y ^ n (0 ≤ x, x ≤ y); 0 ≤ log x (h : 1 ≤ x); 0 < x from h : 2 ≤ x; a + 1 ≤ b + 2 from a ≤ b. Where they differ: (1) For a * c ≤ b * d from 0 ≤ a, a ≤ b, 0 ≤ c, c ≤ d, bound succeeds but gcongr leaves the side goal 0 ≤ b, because its discharger does not chain ha and hab. (2) For 0 < x * x + x from hx : 0 < x, positivity succeeds but bound fails ('aesop failed ... after exhaustive search'). (3) For a + 1 ≤ b + 2 I used gcongr; norm_num. In these tests positivity was the better choice for 0 </≤ goals built from atoms, and bound was better when a side condition had to be derived from the hypotheses.