proposition: Lemma Un_open: forall n:nat, open (Un n).
proof: Proof. destruct n as [|[|]]; trivial. simpl. apply open_full. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology