proposition: Lemma Q_to_Rmult: forall x y, Q_to_R (Qmult x y) = (Rmult (Q_to_R x) (Q_to_R y)).
proof: Proof. intros [ |p|p] [ |p'|p']; try rewrite Q_to_R_Zero; try rewrite Qmult_zero; try rewrite Qmult_zero_right; try rewrite Rmult_0_r; try rewrite Rmult_0_l; try rewrite Q_to_R_Zero; trivial. unfold Q_to_R, numerator, denominator, decode_Q, Qmult, fst, snd; unfold Qpositive_mult. 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 p0')%nat with (S (p0'+p0*(S p0')))%nat; trivial. replace (S q0 * S q0')%nat with (S (q0'+q0*(S q0')))%nat; trivial. set (m:=((p0' + p0 * S p0')%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 Rdiv_Rmult_numerator_denominator; 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 mult_INR. repeat rewrite S_INR. ring. unfold Q_to_R, numerator, denominator, decode_Q, Qmult, fst, snd; unfold Qpositive_mult. 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 p0')%nat with (S (p0'+p0*(S p0')))%nat; trivial. replace (S q0 * S q0')%nat with (S (q0'+q0*(S q0')))%nat; trivial. set (m:=((p0' + p0 * S p0')%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 Rdiv_Rmult_numerator_denominator; 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 mult_INR. repeat rewrite S_INR. ring. unfold Q_to_R, numerator, denominator, decode_Q, Qmult, fst, snd; unfold Qpositive_mult. 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 p0')%nat with (S (p0'+p0*(S p0')))%nat; trivial. replace (S q0 * S q0')%nat with (S (q0'+q0*(S q0')))%nat; trivial. set (m:=((p0' + p0 * S p0')%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 Rdiv_Rmult_numerator_denominator; 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 mult_INR. repeat rewrite S_INR. ring. unfold Q_to_R, numerator, denominator, decode_Q, Qmult, fst, snd; unfold Qpositive_mult. 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 p0')%nat with (S (p0'+p0*(S p0')))%nat; trivial. replace (S q0 * S q0')%nat with (S (q0'+q0*(S q0')))%nat; trivial. set (m:=((p0' + p0 * S p0')%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 Rdiv_Rmult_numerator_denominator; 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 mult_INR. repeat rewrite S_INR. ring. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)