proposition: Lemma Q_to_R_Qone: (Q_to_R Qone=1)%R.
proof: Proof. unfold Q_to_R, numerator, denominator, decode_Q; simpl; field; apply R1_neq_R0. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)