closure of an open interval

[affeldt-aist]

Motivation for this change

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]

@CohenCyril there is this lemma that artificially uses shift and center but I think that it captures well their intended meaning:

Lemma itv_center_shift {R : numFieldType} x y (a b : R) : (a < b) ->
  let c := (a + b) / 2 in let r := (b - a) / 2 in
  Interval (BSide x a) (BSide y b) =
  Interval (BSide x (center r c (*c - r*) )) (BSide y (shift r c (*c + r*))).

It is ok to insist on using shift and center or should you rather strive for generality and put this lemma into unstable.v?

[t6s]

NB: #1848 contains generalization of this PR.