proposition: Lemma expand_U_dyadic_incr: forall f Hopen Hincr n, Included (closure (expand_U_dyadic f Hopen Hincr n)) (expand_U_dyadic f Hopen Hincr (S n)).
proof: Proof. intros. unfold expand_U_dyadic. simpl. destruct even_odd_dec. - destruct normal_sep_fun. simpl. destruct n. + simpl. apply a. + rewrite <- odd_div2. * apply a. * now inversion e. - simpl. destruct normal_sep_fun. simpl. destruct o. rewrite even_div2. + now apply a. + trivial. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology