naming and definition of `monotonous`

[affeldt-aist]

analysis/classical/mathcomp_extra.v

Line 1491 in 437d12c

Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) :=

"According to WP (https://en.wikipedia.org/wiki/Monotonic_function), this should rather be monotonic and I would expect it to be non strict (with homo instead of mono). Maybe we should also have a strict version. I would also expect it to use nondecreasing_fun and the like from realfun.v.
All in all, maybe this change should come in a separate PR so as to not delay the remaining of the current PR." @proux01

[affeldt-aist]

NB: fixing this issue depends on this PR to MathComp math-comp/math-comp#1179