constructor
case h
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101 ∧ g (a - y).val = a
case h.left
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ (a - y).val ∈ Finset.range 101

case h.right
f : ZMod 101 → ℤ
y : ZMod 101
g : ℕ → ZMod 101 := fun i => y + ↑i
hg : ∀ x ∈ Finset.range 101, ∀ y ∈ Finset.range 101, g x = g y → x = y
a : ZMod 101
⊢ g (a - y).val = a