clean up monotonicity lemmas

remove duplicates, rename things more sensibly,
and shorten proofs a little