n - 1 >= 2 - 1 by NAT_2:29, XREAL_1:9;
hence n - 1 is positive ; :: thesis: verum