add `itv_closureE`, `itv_interiorE`, and helper lemmas #571

Job	Run time
rocq-core	1m 4s
coq	1m 1s
mathcomp-classical	3m 4s
mathcomp-analysis-single	15m 32s
mathcomp-reals	4m 5s
mathcomp-reals-stdlib	1m 45s
mathcomp-experimental-reals	1m 59s
mathcomp-analysis	12m 47s
mathcomp-analysis-stdlib	13m 37s
mathcomp-infotheo	7m 2s
	1h 1m 56s

Provide feedback