Slab Arithmetic

theorem EGZ.HasBoundedRepresentative.zero (p K : ℕ) : HasBoundedRepresentative p K 0

theorem EGZ.HasBoundedRepresentative.mono {p K L : ℕ} {a : ZMod p} (ha : HasBoundedRepresentative p K a) (hKL : K ≤ L) : HasBoundedRepresentative p L a

theorem EGZ.HasBoundedRepresentative.neg {p K : ℕ} {a : ZMod p} (ha : HasBoundedRepresentative p K a) : HasBoundedRepresentative p K (-a)

theorem EGZ.HasBoundedRepresentative.add {p K L : ℕ} {a b : ZMod p} (ha : HasBoundedRepresentative p K a) (hb : HasBoundedRepresentative p L b) : HasBoundedRepresentative p (K + L) (a + b)

theorem EGZ.HasBoundedRepresentative.sub {p K L : ℕ} {a b : ZMod p} (ha : HasBoundedRepresentative p K a) (hb : HasBoundedRepresentative p L b) : HasBoundedRepresentative p (K + L) (a - b)

theorem EGZ.HasBoundedRepresentative.int_mul {p K : ℕ} {a : ZMod p} (ha : HasBoundedRepresentative p K a) (n : ℤ) : HasBoundedRepresentative p (n.natAbs * K) (↑n * a)

theorem EGZ.HasBoundedRepresentative.sum {p : ℕ} {I : Type u_1} (s : Finset I) (K : I → ℕ) (a : I → ZMod p) (h : ∀ i ∈ s, HasBoundedRepresentative p (K i) (a i)) : HasBoundedRepresentative p (∑ i ∈ s, K i) (∑ i ∈ s, a i)