proposition: Lemma Q_to_Rminus: forall x y, Q_to_R (Qminus x y) = (Rminus (Q_to_R x) (Q_to_R y)).
proof: Proof. intros x y; unfold Qminus; rewrite Q_to_Rplus; rewrite Q_to_Ropp; trivial. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)