gcongr 'did not make progress' when the bound is a `set` variable

After set A : ℝ≥0∞ := c * X, a goal c * Y ≤ A (from (h1).trans (by gcongr; ...)) fails with 'gcongr did not make progress'. gcongr sees the opaque local A, not c * X, so it finds no matching pattern. Give the monotonicity lemma directly instead. In recent Mathlib, mul_le_mul_right h c : c * a ≤ c * b and mul_le_mul_left h c : a * c ≤ b * c (the primed ENNReal-era names are gone). gcongr also fails when the two sides differ only by a beta-redex, as in ∫ ‖g‖^p * (fun y ↦ w (y+v) ^ s) x versus ∫ ‖g‖^p * w (x+v) ^ s. Nested mul_le_mul_left (...) _ closes it, because exact unifies up to defeq.