1. g : Group{i}
2. e : |g|
3. a : ℤ
4. ¬(a = 0 ∈ ℤ)
⊢ -a x(*;e;~) e = (~ a x(*;e;~) e) ∈ |g|
{ Unfold `int_op` 0 }
1. g : Group{i}
2. e : |g|
3. a : ℤ
4. ¬(a = 0 ∈ ℤ)
⊢ if 0 ≤z -a then -a x(*;e) e else ~ --a x(*;e) e fi = (~ if 0 ≤z a then a x(*;e) e else ~ -a x(*;e) e fi ) ∈ |g|