proposition: Lemma U_dyadic_wd: forall x y:dyadic_rational, dr_eq x y -> U_dyadic x = U_dyadic y.
proof: Proof. intros. induction H; auto. { now transitivity (U_dyadic y). } simpl. unfold packaged_expand_U_dyadic. destruct U_dyadic_level_n. destruct a. simpl. unfold expand_U_dyadic. change ((m + (m + 0))%nat) with ((2*m)%nat). rewrite div2_double. assert (forall m:nat, even (2*m)). { induction m0. { constructor. } replace ((2 * S m0)%nat) with ((S (S (2 * m0)))%nat) by ring. constructor. now constructor. } destruct even_odd_dec; trivial. now contradiction not_even_and_odd with ((2 * m)%nat). Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals TopologicalSpaces InteriorsClosures Div2 Even Arith RTopology