proposition: Lemma Q_to_Rplus: forall x y, Q_to_R (Qplus x y) = (Rplus (Q_to_R x) (Q_to_R y)).
proof: Proof. intros [ |p|p] [ |p'|p']; try rewrite Q_to_R_Zero; try rewrite Qplus_zero_left; try rewrite Qplus_zero_right; try rewrite Rplus_0_r; try rewrite Rplus_0_l; trivial. unfold Q_to_R, numerator, denominator, decode_Q; simpl; field; apply R1_neq_R0... unfold Q_to_R, numerator, denominator, decode_Q, Qplus, fst, snd; unfold Qpositive_plus. destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'. replace (S p0 * S q0' + S p0' * S q0)%nat with (S (q0'+p0*(S q0')+S (q0+p0'*(S q0))))%nat; auto with arith. replace (S q0 * S q0')%nat with (S (q0'+q0*(S q0')))%nat; auto with arith. set (m:=((q0' + p0 * S q0') + S (q0 + p0' * S q0))%nat). set (n:=(q0' + q0 * S q0')%nat). destruct (construct_correct2 (S m+S n) m n (le_n _)) as [factor [H_factor1 H_factor2]]. generalize H_factor1 H_factor2; clear H_factor1 H_factor2. set (P:=(Qpositive_c (S m) (S n) (S m + S n))). destruct (interp_non_zero P) as [P0 [Q0 H'']]. rewrite H''. unfold fst, snd. intros H_factor1 H_factor2. repeat rewrite <- INR_IZR_INZ. rewrite Rplus_Rdiv; auto. rewrite <- (Rdiv_Rmult_simplify (INR (S P0)) (INR (S Q0)) (INR (S factor))); auto. do 2 rewrite <- mult_INR. rewrite <- H_factor1; rewrite <- H_factor2. apply Rmult_Rdiv; auto. subst m n. repeat rewrite S_INR. repeat rewrite plus_INR. repeat rewrite S_INR. repeat rewrite mult_INR. repeat rewrite plus_INR. repeat rewrite mult_INR. repeat rewrite S_INR. ring. unfold Q_to_R at 1, numerator, denominator, decode_Q, Qplus, fst, snd. destruct (Qpositive_le_dec p p') as [H_le_dec|H_le_dec]. destruct (Qpositive_eq_dec p p') as [H_eq_dec|H_eq_dec]. subst p; rewrite Qopp_Qpos; rewrite Q_to_Ropp; rewrite Rplus_opp_r; simpl; field; auto. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. unfold Qpositive_sub. generalize (Qpositive_le_to_Qpositive_le' p p' H_le_dec); unfold Qpositive_le'. generalize (Qpositive_le_noneq_explicit p p' H_le_dec H_eq_dec). destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'; intros H_le_dec_unfolded H_let. assert (H_le_unfold: (S q0' + p0 * S q0' <= q0 + p0' * S q0)%nat); auto with arith. replace (S p0' * S q0 - S p0 * S q0')%nat with (S (q0+p0'*(S q0)- (S q0'+p0*(S q0'))))%nat; [| rewrite <- (Nat.sub_succ_l _ _ H_le_unfold); auto with arith ]. replace (S q0' * S q0)%nat with (S (q0+q0'*(S q0)))%nat; auto with arith. replace (S p0' * S q0 + S p0 * S q0')%nat with (S (q0+p0'*(S q0)+S (q0'+p0*(S q0'))))%nat; auto with arith. set (m':=((q0 + p0' * S q0) + S (q0' + p0 * S q0'))%nat). set (m:=((q0 + p0' * S q0) - (S q0' + p0 * S q0'))%nat). set (n:=(q0 + q0' * S q0)%nat). assert (H_m':(S m + S n <= S m' + S n)%nat); [ subst m m' n; apply Nat.add_le_mono_r; apply le_n_S; apply Nat.le_trans with (q0 + p0' * S q0)%nat; auto with arith; apply Nat.le_sub_l |]. destruct (construct_correct2 (S m'+S n) m n H_m') as [factor [H_factor1 H_factor2]]. generalize H_factor1 H_factor2; clear H_factor1 H_factor2. set (P:=(Qpositive_c (S m) (S n) (S m' + S n))). destruct (interp_non_zero P) as [P0 [Q0 H'']]. rewrite H''. unfold fst, snd. intros H_factor1 H_factor2. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. rewrite Rplus_Rdiv; auto. rewrite <- (Rdiv_Rmult_simplify (- INR (S P0)) (INR (S Q0)) (INR (S factor))); auto. rewrite Ropp_mult_distr_l_reverse; do 2 rewrite <- mult_INR. rewrite <- H_factor1; rewrite <- H_factor2. apply Rmult_Rdiv; auto. subst m n. repeat rewrite S_INR. rewrite minus_INR; trivial. repeat rewrite plus_INR. repeat rewrite mult_INR. repeat rewrite S_INR. ring. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. unfold Qpositive_sub. generalize (sym_not_eq (not_Qpositive_le_not_eq _ _ H_le_dec)). generalize (not_Qpositive_le_Qpositive_le' _ _ H_le_dec); clear H_le_dec; intros H_le_dec H_eq_dec. generalize (Qpositive_le_to_Qpositive_le' p' p H_le_dec); unfold Qpositive_le'. generalize (Qpositive_le_noneq_explicit p' p H_le_dec H_eq_dec). destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'; intros H_le_dec_unfolded H_lt. assert (H_le_unfold: (S q0 + p0' * S q0 <= q0' + p0 * S q0')%nat); auto with arith. replace (S p0 * S q0' - S p0' * S q0)%nat with (S (q0'+p0*(S q0')- (S q0+p0'*(S q0))))%nat; [| rewrite <- (Nat.sub_succ_l _ _ H_le_unfold); auto with arith ]. replace (S q0 * S q0')%nat with (S (q0'+q0*(S q0')))%nat; auto with arith. replace (S p0 * S q0' + S p0' * S q0)%nat with (S (q0'+p0*(S q0')+S (q0+p0'*(S q0))))%nat; auto with arith. set (m':=((q0' + p0 * S q0') + S (q0 + p0' * S q0))%nat). set (m:=((q0' + p0 * S q0') - (S q0 + p0' * S q0))%nat). set (n:=(q0' + q0 * S q0')%nat). assert (H_m':(S m + S n <= S m' + S n)%nat); [ subst m m' n; apply Nat.add_le_mono_r; apply le_n_S; apply Nat.le_trans with (q0' + p0 * S q0')%nat; auto with arith; apply Nat.le_sub_l |]. destruct (construct_correct2 (S m'+S n) m n H_m') as [factor [H_factor1 H_factor2]]. generalize H_factor1 H_factor2; clear H_factor1 H_factor2. set (P:=(Qpositive_c (S m) (S n) (S m' + S n))). destruct (interp_non_zero P) as [P0 [Q0 H'']]. rewrite H''. unfold fst, snd. intros H_factor1 H_factor2. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. rewrite Rplus_Rdiv; auto. rewrite <- (Rdiv_Rmult_simplify (INR (S P0)) (INR (S Q0)) (INR (S factor))); auto. rewrite Ropp_mult_distr_l_reverse; do 2 rewrite <- mult_INR. rewrite <- H_factor1; rewrite <- H_factor2. apply Rmult_Rdiv; auto. subst m n. repeat rewrite S_INR. rewrite minus_INR; trivial. repeat rewrite plus_INR. repeat rewrite mult_INR. repeat rewrite S_INR. ring. unfold Q_to_R at 1, numerator, denominator, decode_Q, Qplus, fst, snd. destruct (Qpositive_le_dec p p') as [H_le_dec|H_le_dec]. destruct (Qpositive_eq_dec p p') as [H_eq_dec|H_eq_dec]. subst p; rewrite Qopp_Qpos; rewrite Q_to_Ropp; rewrite Rplus_opp_l; simpl; field; auto. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. unfold Qpositive_sub. generalize (Qpositive_le_to_Qpositive_le' p p' H_le_dec); unfold Qpositive_le'. generalize (Qpositive_le_noneq_explicit p p' H_le_dec H_eq_dec). destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'; intros H_le_dec_unfolded H_let. assert (H_le_unfold: (S q0' + p0 * S q0' <= q0 + p0' * S q0)%nat); auto with arith. replace (S p0' * S q0 - S p0 * S q0')%nat with (S (q0+p0'*(S q0)- (S q0'+p0*(S q0'))))%nat; [| rewrite <- (Nat.sub_succ_l _ _ H_le_unfold); auto with arith ]. replace (S q0' * S q0)%nat with (S (q0+q0'*(S q0)))%nat; auto with arith. replace (S p0' * S q0 + S p0 * S q0')%nat with (S (q0+p0'*(S q0)+S (q0'+p0*(S q0'))))%nat; auto with arith. set (m':=((q0 + p0' * S q0) + S (q0' + p0 * S q0'))%nat). set (m:=((q0 + p0' * S q0) - (S q0' + p0 * S q0'))%nat). set (n:=(q0 + q0' * S q0)%nat). assert (H_m':(S m + S n <= S m' + S n)%nat); [ subst m m' n; apply Nat.add_le_mono_r; apply le_n_S; apply Nat.le_trans with (q0 + p0' * S q0)%nat; auto with arith; apply Nat.le_sub_l |]. destruct (construct_correct2 (S m'+S n) m n H_m') as [factor [H_factor1 H_factor2]]. generalize H_factor1 H_factor2; clear H_factor1 H_factor2. set (P:=(Qpositive_c (S m) (S n) (S m' + S n))). destruct (interp_non_zero P) as [P0 [Q0 H'']]. rewrite H''. unfold fst, snd. intros H_factor1 H_factor2. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. rewrite Rplus_Rdiv; auto. rewrite <- (Rdiv_Rmult_simplify (INR (S P0)) (INR (S Q0)) (INR (S factor))); auto. rewrite Ropp_mult_distr_l_reverse; do 2 rewrite <- mult_INR. rewrite <- H_factor1; rewrite <- H_factor2. apply Rmult_Rdiv; auto. subst m n. repeat rewrite S_INR. rewrite minus_INR; trivial. repeat rewrite plus_INR. repeat rewrite mult_INR. repeat rewrite S_INR. ring. unfold Q_to_R, numerator, denominator, decode_Q, fst, snd. unfold Qpositive_sub. generalize (sym_not_eq (not_Qpositive_le_not_eq _ _ H_le_dec)). generalize (not_Qpositive_le_Qpositive_le' _ _ H_le_dec); clear H_le_dec; intros H_le_dec H_eq_dec. generalize (Qpositive_le_to_Qpositive_le' p' p H_le_dec); unfold Qpositive_le'. generalize (Qpositive_le_noneq_explicit p' p H_le_dec H_eq_dec). destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'; intros H_le_dec_unfolded H_lt. assert (H_le_unfold: (S q0 + p0' * S q0 <= q0' + p0 * S q0')%nat); auto with arith. replace (S p0 * S q0' - S p0' * S q0)%nat with (S (q0'+p0*(S q0')- (S q0+p0'*(S q0))))%nat; [| rewrite <- (Nat.sub_succ_l _ _ H_le_unfold); auto with arith ]. replace (S q0 * S q0')%nat with (S (q0'+q0*(S q0')))%nat; auto with arith. replace (S p0 * S q0' + S p0' * S q0)%nat with (S (q0'+p0*(S q0')+S (q0+p0'*(S q0))))%nat; auto with arith. set (m':=((q0' + p0 * S q0') + S (q0 + p0' * S q0))%nat). set (m:=((q0' + p0 * S q0') - (S q0 + p0' * S q0))%nat). set (n:=(q0' + q0 * S q0')%nat). assert (H_m':(S m + S n <= S m' + S n)%nat); [ subst m m' n; apply Nat.add_le_mono_r; apply le_n_S; apply Nat.le_trans with (q0' + p0 * S q0')%nat; auto with arith; apply Nat.le_sub_l |]. destruct (construct_correct2 (S m'+S n) m n H_m') as [factor [H_factor1 H_factor2]]. generalize H_factor1 H_factor2; clear H_factor1 H_factor2. set (P:=(Qpositive_c (S m) (S n) (S m' + S n))). destruct (interp_non_zero P) as [P0 [Q0 H'']]. rewrite H''. unfold fst, snd. intros H_factor1 H_factor2. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. rewrite Rplus_Rdiv; auto. rewrite <- (Rdiv_Rmult_simplify (-INR (S P0)) (INR (S Q0)) (INR (S factor))); auto. rewrite Ropp_mult_distr_l_reverse; do 2 rewrite <- mult_INR. rewrite <- H_factor1; rewrite <- H_factor2. apply Rmult_Rdiv; auto. subst m n. repeat rewrite S_INR. rewrite minus_INR; trivial. repeat rewrite plus_INR. repeat rewrite mult_INR. repeat rewrite S_INR. ring. unfold Q_to_R, numerator, denominator, decode_Q, Qplus, fst, snd; unfold Qpositive_plus. destruct (interp_non_zero p) as [p0 [q0 H]]. destruct (interp_non_zero p') as [p0' [q0' H']]. rewrite H; rewrite H'. replace (S p0 * S q0' + S p0' * S q0)%nat with (S (q0'+p0*(S q0')+S (q0+p0'*(S q0))))%nat; auto with arith. replace (S q0 * S q0')%nat with (S (q0'+q0*(S q0')))%nat; auto with arith. set (m:=((q0' + p0 * S q0') + S (q0 + p0' * S q0))%nat). set (n:=(q0' + q0 * S q0')%nat). destruct (construct_correct2 (S m+S n) m n (le_n _)) as [factor [H_factor1 H_factor2]]. generalize H_factor1 H_factor2; clear H_factor1 H_factor2. set (P:=(Qpositive_c (S m) (S n) (S m + S n))). destruct (interp_non_zero P) as [P0 [Q0 H'']]. rewrite H''. unfold fst, snd. intros H_factor1 H_factor2. repeat rewrite Ropp_Ropp_IZR; repeat rewrite <- INR_IZR_INZ. rewrite Rplus_Rdiv; auto. rewrite <- (Rdiv_Rmult_simplify (-INR (S P0)) (INR (S Q0)) (INR (S factor))); auto. rewrite Ropp_mult_distr_l_reverse; do 2 rewrite <- mult_INR. rewrite <- H_factor1; rewrite <- H_factor2. apply Rmult_Rdiv; auto. subst m n. repeat rewrite S_INR. repeat rewrite plus_INR. repeat rewrite S_INR. repeat rewrite mult_INR. repeat rewrite plus_INR. repeat rewrite mult_INR. repeat rewrite S_INR. ring. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)