mono [D, R: TYPE FROM real]: THEORY BEGIN f, g: VAR [D -> R] x, x1, x2: VAR D y: VAR R monotonic_incr?(f): bool = (FORALL x1,x2: x1 < x2 IMPLIES f(x1) < f(x2)) monotonic_decr?(f): bool = (FORALL x1,x2: x1 < x2 IMPLIES f(x1) > f(x2)) monotonic?(f): bool = monotonic_incr?(f) OR monotonic_decr?(f) mono_is_inj: LEMMA monotonic?(f) IMPLIES injective?(f) END mono