proposition: Lemma Q_to_Rdiv: forall x y, ~(y=Zero) -> Q_to_R (Qdiv x y) = (Rdiv (Q_to_R x) (Q_to_R y)).
proof: Proof. intros x y Hy; unfold Qdiv; rewrite Q_to_Rmult; rewrite Q_to_Rinv; trivial. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)