let m, n be Nat; :: thesis: - (m * ((- 1) to_power n)) >= - m
( 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 * ((- 1) to_power n)) >= - m ; :: thesis: verum