proposition: Lemma Q_to_R_Qneq:forall x y : Q, (Q_to_R x)<>(Q_to_R y) -> x<>y.
proof: Proof. intros x y H_Rneq; contradict H_Rneq; rewrite H_Rneq; trivial. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)