fact: Definition Un (n:nat) : Ensemble X := match n with | O => U0 | S O => U1 | S (S _) => Full_set end.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology