fixes #1133

[affeldt-aist]

Motivation for this change

fixes #1133

the existing (ill-named) monotonous corresponds to
a strict version of monotonicity (using mono/ <=)

following the conversation in issue
#1133
this PR:

• introduces the new definition monotonic
  (non strict, using homo instead of mono)
• renames monotonous into strict_monotonic
  and redefines it using homo/< instead of mono/<=
• adjust lemmas in num_normedtype.v and realfun.v
• in particular, in num_normedtype.v:
  • weaken hypo in lemma mono_mem_image_segment
  • weaken hypo in lemma mono_surj_image_segment
  • weaken hypo in lemma inc_surj_image_segment
  • weaken hypo in lemma dec_surj_image_segment
  • weaken hypo in lemma inc_surj_image_segmentP
  • weaken hypo in lemma dec_surj_image_segmentP
  • weaken hypo in lemma mono_surj_image_segmentP

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

Since this is an old issue, since it corrects a naming error that is detrimental to users, since it weakens the hypotheses of a few lemmas, we can maybe merge it in the interest of the release.

[proux01]

Indeed, let's merge