let m, n be Nat; :: thesis: - m <= m * ((- 1) to_power n)
( n is even or n is odd ) ;
then ( (- 1) to_power n = 1 or (- 1) to_power n = - 1 ) by FIB_NUM2:2, FIB_NUM2:3;
hence - m <= m * ((- 1) to_power n) ; :: thesis: verum