proposition: Lemma Q_to_R_not_eq: forall x y, ~(x=y)->~(Q_to_R x = Q_to_R y).
proof: Proof. intros [ |p|p] [ |p'|p'] H_not_eq. apply False_ind; apply H_not_eq; trivial. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. destruct (interp_non_zero p') as [p0 [q0 H]]. rewrite H. repeat rewrite <- INR_IZR_INZ. apply Rlt_not_eq; stepl R0; [|simpl; field]; 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]]. rewrite H. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. apply Rlt_not_eq'. apply Ropp_lt_cancel. stepl R0; [|simpl; field]; 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]]. rewrite H. repeat rewrite <- INR_IZR_INZ. apply Rlt_not_eq'. stepl R0; [|simpl; field]; unfold Rdiv; apply Fourier_util.Rlt_mult_inv_pos; auto. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. destruct (not_Qeq_inf _ _ H_not_eq) as [H_Q_lt|H_Q_lt]; 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; [ apply Rlt_not_eq | apply Rlt_not_eq']; 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. destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. apply Rlt_not_eq'. 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. destruct (interp_non_zero p) as [p0 [q0 H]]. rewrite H. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. apply Rlt_not_eq. apply Ropp_lt_cancel. stepl R0; [|simpl; field]; 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'. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. apply Rlt_not_eq. 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. destruct (not_Qeq_inf _ _ H_not_eq) as [H_Q_lt|H_Q_lt]; 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; [ apply Rlt_not_eq | apply Rlt_not_eq']; 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... 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)