let s be Nat; :: thesis: for n being odd Nat st s >= 2 holds
n divides Polygon (s,n)
let n be odd Nat; :: thesis: ( s >= 2 implies n divides Polygon (s,n) )
assume A1: s >= 2 ; :: thesis: n divides Polygon (s,n)
A2: Polygon (s,n) = (((n * (s - 2)) * (n - 1)) / 2) + n ;
A3: s - 0 >= 2 by A1;
then s - 2 >= 0 by XREAL_1:11;
then A4: (n * (s - 2)) * (n - 1) in NAT by INT_1:3;
reconsider k = ((n * (s - 2)) * (n - 1)) / 2 as Nat by A4;
A5: s - 2 in NAT by INT_1:3, A3, XREAL_1:11;
k = n * ((s - 2) * ((n - 1) / 2)) ;
then n divides k by NAT_D:def 3, A5;
hence n divides Polygon (s,n) by A2, NAT_D:8; :: thesis: verum