proposition: Lemma Q_to_Rlt: forall x y, Qlt x y -> Rlt (Q_to_R x) (Q_to_R y).
proof: Proof. intros [ |p|p] [ |p'|p'] H_Q_lt; try solve [ apply False_ind; apply (Qlt_irreflexive Zero); trivial | apply False_ind; apply (Qlt_irreflexive Zero); apply Qlt_transitive with (Qneg p'); trivial | apply False_ind; apply (Qlt_irreflexive Zero); apply Qlt_transitive with (Qpos p); trivial | apply False_ind; apply (Qlt_irreflexive (Qpos p)); apply Qlt_transitive with (Qneg p'); trivial ]. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. simpl; destruct (interp_non_zero p') as [p0 [q0 H]]. rewrite H; repeat rewrite <- INR_IZR_INZ. stepl R0; try field; auto. unfold Rdiv; apply Fourier_util.Rlt_mult_inv_pos; auto. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. inversion_clear H_Q_lt as [x y H_not_le| | | | ]. generalize (sym_not_eq (not_Qpositive_le_not_eq _ _ H_not_le)). generalize (not_Qpositive_le_Qpositive_le' _ _ H_not_le). intros H_Q_le H_neq. generalize (Qpositive_le_noneq_explicit _ _ H_Q_le H_neq). destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'; intro H_Q_lt_unfold. repeat rewrite <- INR_IZR_INZ. apply Rmult_Rdiv_pos_Rlt; auto. repeat rewrite <- mult_INR. apply lt_INR; trivial. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. simpl; destruct (interp_non_zero p) as [p0 [q0 H]]. rewrite H; rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. apply Ropp_lt_cancel. stepl R0; try field; auto. stepr (INR (S p0) / INR (S q0))%R; [|field; auto]. unfold Rdiv; apply Fourier_util.Rlt_mult_inv_pos; auto. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'. rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. apply Rlt_trans with R0. apply Ropp_lt_cancel; stepl R0; try field; auto; stepr (INR (S p0) / INR (S q0))%R; [|field; auto]; unfold Rdiv; apply Fourier_util.Rlt_mult_inv_pos; auto. stepl R0; try field; auto; unfold Rdiv; apply Fourier_util.Rlt_mult_inv_pos; auto. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. inversion_clear H_Q_lt as [ |x y H_not_le| | | ]. generalize (sym_not_eq (not_Qpositive_le_not_eq _ _ H_not_le)). generalize (not_Qpositive_le_Qpositive_le' _ _ H_not_le). intros H_Q_le H_neq. generalize (Qpositive_le_noneq_explicit _ _ H_Q_le H_neq). destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'; intro H_Q_lt_unfold. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. apply Rmult_Rdiv_pos_Rlt; auto. apply Ropp_lt_cancel. stepr (INR (S p0) * INR (S q0'))%R; [|field; auto]. stepl (INR (S p0') * INR (S q0))%R; [|field; auto]. repeat rewrite <- mult_INR. apply lt_INR; trivial. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)