let n be non zero Nat; :: thesis: ( n > 2 implies not Dihedral_group n is commutative )
assume A1: n > 2 ; :: thesis: not Dihedral_group n is commutative
then 1 < n by XXREAL_0:2;
then 1 in Segm n by NAT_1:44;
then 1 in the carrier of (INT.Group n) by Th76;
then reconsider g1 = 1 as Element of (INT.Group n) ;
1 in INT.Group 2 by EltsOfINTGroup2;
then reconsider a2 = 1 as Element of (INT.Group 2) ;
reconsider x = <*g1,(1_ (INT.Group 2))*>, y = <*(1_ (INT.Group n)),a2*> as Element of (Dihedral_group n) by Th9;
y * x <> x * y

proof

x |^ (n - 1) <> x

proof

assume x |^ (n - 1) = x ; :: thesis: contradiction
then B1: x * x = x |^ ((n - 1) + 1) by GROUP_1:34
.= 1_ (Dihedral_group n) by Th101 ;
x |^ 2 <> 1_ (Dihedral_group n) by A1, Th102;
then x * x <> 1_ (Dihedral_group n) by GROUP_1:27;
hence contradiction by B1; :: thesis: verum

end;

then x |^ (n - 1) <> x ;
then A3: (x |^ (n - 1)) * y <> x * y by GROUP_1:6;
y * x = (x |^ (n - 1)) * y by Th100;
hence y * x <> x * y by A3; :: thesis: verum

end;

hence not Dihedral_group n is commutative ; :: thesis: verum