proposition: Lemma dr_total_order: forall x y:dyadic_rational, dr_lt x y \/ dr_eq x y \/ dr_lt y x.
proof: Proof. intros. destruct x as [m n]. destruct y as [m' n']. destruct (Nat.le_gt_cases n n'). - destruct (dr_incr_denom m n n') as [m0]; trivial. destruct (Nat.le_gt_cases m0 m'). + apply Nat.lt_eq_cases in H1. destruct H1. * left. apply dr_lt_wd with (m_over_2_to_n m0 n') (m_over_2_to_n m' n'); trivial. -- apply intro_dr_lt; trivial. -- apply dr_eq_refl. * right; left. apply dr_eq_trans with (m_over_2_to_n m0 n'). -- apply dr_eq_sym; trivial. -- rewrite H1; apply dr_eq_refl. + right; right. apply dr_lt_wd with (m_over_2_to_n m' n') (m_over_2_to_n m0 n'); trivial. * apply intro_dr_lt; trivial. * apply dr_eq_refl. - assert (n' <= n) by auto with arith. destruct (dr_incr_denom m' n' n) as [m0]; trivial. destruct (Nat.le_gt_cases m m0). + apply Nat.lt_eq_cases in H2. destruct H2. * left. apply dr_lt_wd with (m_over_2_to_n m n) (m_over_2_to_n m0 n). -- apply intro_dr_lt; trivial. -- apply dr_eq_refl. -- trivial. * right; left. apply dr_eq_trans with (m_over_2_to_n m0 n); trivial. rewrite H2; apply dr_eq_refl. + right; right. apply dr_lt_wd with (m_over_2_to_n m0 n) (m_over_2_to_n m n); trivial. * apply intro_dr_lt; trivial. * apply dr_eq_refl. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals