take - 1 ; :: thesis: - 1 is negative
thus - 1 is negative by XXREAL_0:def 7; :: thesis: verum