proposition: Lemma Un_incr: forall n:nat, Included (closure (Un n)) (Un (S n)).
proof: Proof. destruct n as [|]. - simpl. trivial. - simpl. red; intros; constructor. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology