m n a✝ b✝ c d a b : ℤ
hb : 0 < b
this : a % b < abs b
⊢ a % b < b
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
⊢ a % b < b
have : a % b < |b| := emod_lt _ (ne_of_gt hb)
no goals
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
this : a % b < abs b
⊢ a % b < b
rwa [abs_of_pos hb] at this
no goals
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
⊢ a % b ≡ a [ZMOD b]
simp [ModEq]