proposition: Lemma Q_to_R_Qeq:forall x y : Q, (Q_to_R x)=(Q_to_R y) -> x=y.
proof: Proof. intros x y H_Req; destruct (Q_eq_dec x y) as [Hxy|Hxy]; trivial; apply False_ind; apply (Q_to_R_not_eq _ _ Hxy); assumption. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)