proposition: Lemma Q_to_Rinv: forall x, ~(x=Zero) -> Q_to_R (Qinv x) = Rinv (Q_to_R x).
proof: Proof. intros [ |p|p] H_zero. apply False_ind; auto. unfold Q_to_R, numerator, denominator, decode_Q, Qinv, fst, snd. destruct (interp_non_zero p) as [p0 [q0 H]]. rewrite (inv_correct p _ _ H); rewrite H. repeat rewrite <- INR_IZR_INZ. rewrite Rinv_div; auto. unfold Q_to_R, numerator, denominator, decode_Q, Qinv, fst, snd. destruct (interp_non_zero p) as [p0 [q0 H]]. rewrite (inv_correct p _ _ H); rewrite H. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. rewrite Rinv_div; auto. unfold Rdiv; rewrite <- Rmult_opp_opp; rewrite Ropp_involutive; rewrite Rinv_opp; auto. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)