take ArProg (0,(- 1)) ; :: thesis: ( ArProg (0,(- 1)) is decreasing & ArProg (0,(- 1)) is non-increasing )
thus ( ArProg (0,(- 1)) is decreasing & ArProg (0,(- 1)) is non-increasing ) ; :: thesis: verum