proposition: Lemma Interval_ereal_mem (r : R) (a b : itv_bound R) : r \in Interval a b -> (a <= r%:E <= b)%E.
proof: Proof. case: a b => [[] a|[]] [[] b|[]] => /[dup] rab /itvP rw//=; by rewrite ?lee_fin ?rw//= ?leey ?leNye//; move: rab; rewrite in_itv//= andbF. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) HB(structures) reals ereal signed topology normedtype sequences