1. g : Group{i}
2. e : |g|
3. a : ℤ
⊢ -a x(*;e;~) e = (~ a x(*;e;~) e) ∈ |g|
{ Decide a = 0 ∈ ℤ THENA Auto }
1. g : Group{i}
2. e : |g|
3. a : ℤ
4. a = 0 ∈ ℤ
⊢ -a x(*;e;~) e = (~ a x(*;e;~) e) ∈ |g|
1. g : Group{i}
2. e : |g|
3. a : ℤ
4. ¬(a = 0 ∈ ℤ)
⊢ -a x(*;e;~) e = (~ a x(*;e;~) e) ∈ |g|