proposition: Lemma expand_U_dyadic_open: forall f Hopen Hincr n, open (expand_U_dyadic f Hopen Hincr n).
proof: Proof. intros. unfold expand_U_dyadic. destruct even_odd_dec. - apply Hopen. - destruct normal_sep_fun. simpl. apply a. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology