proposition: Lemma U_dyadic_open: forall x:dyadic_rational, open (U_dyadic x).
proof: Proof. intro. destruct x. unfold U_dyadic. now destruct U_dyadic_level_n. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology