no goals
m n a✝ b✝ c d a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑(natAbs z) < b ∧ ↑(natAbs z) ≡ a [ZMOD b]
constructor <;> rw [ofNat_natAbs_eq_of_nonneg z hz1] <;> assumption