proposition: Lemma dr_incr_denom: forall (m n n':nat), n<=n' -> exists m':nat, dr_eq (m_over_2_to_n m' n') (m_over_2_to_n m n).
proof: Proof. induction 1. - exists m. apply dr_eq_refl. - destruct IHle as [m']. exists (2*m'). apply dr_eq_trans with (m_over_2_to_n m' m0); trivial. apply dr_eq_sym. apply dr_eq_scale. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals