The @[mono] attribute #
A lemma stating the monotonicity of some function, with respect to appropriate relations on its domain and range, and possibly with side conditions.
Instances For
A lemma stating the monotonicity of some function, with respect to appropriate relations on its domain and range, and possibly with side conditions.