let k, n be Nat; :: thesis: (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n)
k * (2 |^ (n + 1)) = k * ((2 |^ n) * 2) by NEWTON:6
.= (k * (2 |^ n)) * 2 ;
hence (k * (2 |^ (n + 1))) div 2 = k * (2 |^ n) ; :: thesis: verum