let G be _Graph; :: thesis: for W being Walk of G
for n being odd Element of NAT st n <= len W holds
( (2 * ((n + 1) div 2)) - 1 = n & 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (W .vertexSeq()) )
let W be Walk of G; :: thesis: for n being odd Element of NAT st n <= len W holds
( (2 * ((n + 1) div 2)) - 1 = n & 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (W .vertexSeq()) )
let n be odd Element of NAT ; :: thesis: ( n <= len W implies ( (2 * ((n + 1) div 2)) - 1 = n & 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (W .vertexSeq()) ) )
assume A1: n <= len W ; :: thesis: ( (2 * ((n + 1) div 2)) - 1 = n & 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (W .vertexSeq()) )
set m = (n + 1) div 2;
2 divides n + 1 by PEPIN:22;
then A2: 2 * ((n + 1) div 2) = n + 1 by NAT_D:3;
hence (2 * ((n + 1) div 2)) - 1 = n ; :: thesis: ( 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (W .vertexSeq()) )
A3: now :: thesis: not (n + 1) div 2 < 1
assume (n + 1) div 2 < 1 ; :: thesis: contradiction
then (n + 1) div 2 < 0 + 1 ;
then (n + 1) div 2 = 0 by NAT_1:13;
hence contradiction by A2; :: thesis: verum
end;
then reconsider maa1 = ((n + 1) div 2) - 1 as Element of NAT by INT_1:5;
thus 1 <= (n + 1) div 2 by A3; :: thesis: (n + 1) div 2 <= len (W .vertexSeq())
now :: thesis: not len (W .vertexSeq()) < (n + 1) div 2
assume len (W .vertexSeq()) < (n + 1) div 2 ; :: thesis: contradiction
then len (W .vertexSeq()) < maa1 + 1 ;
then len (W .vertexSeq()) <= maa1 by NAT_1:13;
then 2 * (len (W .vertexSeq())) <= 2 * maa1 by NAT_1:4;
then (len W) + 1 <= (2 * ((n + 1) div 2)) - (2 * 1) by Def14;
then ((len W) + 1) + 2 <= ((n + 1) - 2) + 2 by A2, XREAL_1:7;
then ((len W) + 1) + 2 < (n + 1) + 1 by NAT_1:13;
then ((len W) + 3) - 3 < (n + 2) - 2 by XREAL_1:14;
hence contradiction by A1; :: thesis: verum
end;
hence (n + 1) div 2 <= len (W .vertexSeq()) ; :: thesis: verum