proposition: Lemma Q_to_Req: forall x y, @eq Q x y -> ((Q_to_R x)=(Q_to_R y))%R.
proof: Proof. exact (f_equal Q_to_R). Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)