theorem Th117: :: GROUP_24:112

for n being non zero odd Nat
for g1 being Element of (INT.Group n) st g1 = 1 holds
for x being Element of (Dihedral_group n) st x = <*g1,(1_ (INT.Group 2))*> holds
for i being Nat holds
( not i < n or i = 0 or x |^ i <> x |^ (n - i) )