change inequality in ereal_{d,}nbhs and {p,n}infty_{d,}nbhs

[affeldt-aist]

• from strict to large
• also adds a few lemmas to ereal.v

closed #122 @CohenCyril

This is globally getting a bit bigger (only a few proofs are shortened). I have maybe not been careful enough when updating.

[affeldt-aist]

IIRC, the problem with this PR is that it does not bring the expected code size reduction. But there is now code size augmentation (except with one lemma). Since we all seem to agree that large inequalities fell better suited, we can maybe merge this PR for now. What do you think?

[CohenCyril]

I think this PR essentially exibits a lack of abstraction. We should actually understand how to make the code smaller, and I think it might not be about changing the def.