proposition: Lemma eq_inject_Q : forall {R : ConstructiveReals} (q r : Q), CR_of_Q R q == CR_of_Q R r -> Qeq q r.
proof: Proof. intros. destruct H. destruct (Q_dec q r). - destruct s. + exfalso. apply (CR_of_Q_lt R q r) in q0. contradiction. + exfalso. apply (CR_of_Q_lt R r q) in q0. contradiction. - exact q0. Qed.
imports: QArith Qabs Qround