proposition: Lemma U_dyadic_incr: forall x y:dyadic_rational, dr_lt x y -> Included (closure (U_dyadic x)) (U_dyadic y).
proof: Proof. intros. induction H. - induction H. + unfold U_dyadic. destruct U_dyadic_level_n. simpl. apply a. + cut (Included (closure (U_dyadic (m_over_2_to_n m0 n))) (U_dyadic (m_over_2_to_n (S m0) n))). * intro. pose proof (closure_inflationary (U_dyadic (m_over_2_to_n m0 n))). auto with sets. * unfold U_dyadic. destruct U_dyadic_level_n. simpl. apply a. - now rewrite <- (U_dyadic_wd _ _ H0), <- (U_dyadic_wd _ _ H1). Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology