gcongr failure

Stream: mathlib4

[Jeremy Tan]

This theorem should be provable by gcongr as there is a proof term using only congruence lemmas in gcongr's set, but gcongr does not remove anything beyond the ceiling signs:

import Mathlib.Data.Rat.Floor

open Int

lemma pass {b v r : ℚ} (hb : 0 ≤ b) (hr : 0 ≤ r) : ⌈(0 - v) / r⌉ ≤ ⌈(b - v) / r⌉ :=
  ceil_le_ceil _ _ <| div_le_div_of_le hr <| sub_le_sub_right hb v

lemma fail {b v r : ℚ} (hb : 0 ≤ b) (hr : 0 ≤ r) : ⌈(0 - v) / r⌉ ≤ ⌈(b - v) / r⌉ := by
  gcongr
  -- (0 - v) / r ≤ (b - v) / r
  gcongr -- fails

@Heather Macbeth?

[Jeremy Tan]

Context is https://github.com/leanprover-community/mathlib4/pull/9348/files#diff-d5d2cf7fb7cd3b433e15c84d5103ebcda0f770037f46f93afa6aab1bd2a62ea0R113-R114

[Yury G. Kudryashov]

attribute [gcongr] div_le_div_of_le_of_nonneg fixes it

[Yury G. Kudryashov]

It would be nice if you add @[gcongr] to other relevant lemmas in that file too.