take <%0_No%> ; :: thesis: <%0_No%> is strictly_decreasing
thus <%0_No%> is strictly_decreasing ; :: thesis: verum