affeldt-aist

The topic again popped up in the conversion of PR #1147: "On a topological note, the "right-sided topology on R" AKA the "Sogenfrey line" captures a lot of this nicely....

It also looks like `\forall x \near F, P x` always displays as `\near F, P F` (unless `F` is a composed expression such as `nbhs X` or `f @...

side question: would it be bad to get rid of the `\near F, P F`?

By the way, I was looking for a way to infer a `{nonneg R}` from a `{i01 R}`.

NB: If one change pointed to choice in `measure.v`, all `measure.v` but one lemma and all `measure_lebesgue.v` go through. `lebesgue_integral.v` fails at https://github.com/math-comp/analysis/blob/f42137704caa1d97eff6a1670e7a664a548c98c2/theories/lebesgue_integral.v#L262 where pointed it needed to have the...

Why does the `1 != 0` property belong to the mixin of rings?

Observation by @t6s : it should be easy to insert an intermediate mixin for non-necessarily not-trivial rings once MathComp 2.0 is available.

I didn't mean to sound catastrophic ^_^, I just thought that it might be a good timing to think of a name change, I don't think that the `semi_` prefix...

> There is certainly more to do since some definitions in `pred` duplicate existing definitions in `set` (upper_bound vs. ubound, nonempty, etc.). This topic was discussed during a mathcomp-analysis-dev meeting:...

@ggonthier ok with merging?