proposition: Lemma is_intervalPlt (E : set R) : is_interval E <-> forall x y, E x -> E y -> forall z, x < z < y -> E z.
proof: Proof. split=> iE x y Ex Ey z /andP[]. by move=> xz zy; apply: (iE x y); rewrite ?ltW. rewrite !le_eqVlt => /predU1P[<-//|xz] /predU1P[->//|zy]. by apply: (iE x y); rewrite ?xz. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule