proposition: Lemma itv_oNyy : `]-oo%E, +oo[%classic = ~` [set -oo]%E :> set (\bar R).
proof: Proof. rewrite set_itvE predeqE => x; split => /=. - by move: x => [x| |]; rewrite ?ltxx. - by move: x => [x h|//|/(_ erefl)]; rewrite ?ltNyr. 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