proposition: Lemma Incl_T_absorbs_Is_refining_T_R:forall xi, Incl_T xi RR -> Is_refining_T (m_product inv_RR xi).
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))). unfold Incl_T, Is_refining_T, Bounded_T, m_product, inv_digit, map_digits, inv_RR, fst, snd. replace (1/2 - 1/2) with Zero; [|qZ_numerals; field; auto]; replace (-1/2 + 3/2) with Qone; [|qZ_numerals; field; auto]; replace (3/2 - -1/2) with (Qone +Qone); [|qZ_numerals; field; auto]; replace (1/2 + 1/2) with Qone; [|qZ_numerals; field; auto]; repeat rewrite Qmult_one_right. intros [[[H1 [H2 [H3 H4]]]|[H1 [H2 [H3 H4]]]] [H5 [H6 [H7 [H8 [H9 [H10 [H11 H12]]]]]]]]. generalize (Qmult_resp_Qle_pos_l _ _ _ H2 H5); generalize (Qmult_resp_Qle_pos_l _ _ _ H2 H6); generalize (Qmult_resp_Qle_pos_l _ _ _ H3 H7); generalize (Qmult_resp_Qle_pos_l _ _ _ H3 H8); generalize (Qmult_resp_Qle_pos_l _ _ _ H4 H9); generalize (Qmult_resp_Qle_pos_l _ _ _ H4 H10); generalize (Qmult_resp_Qle_pos_l _ _ _ H1 H11); generalize (Qmult_resp_Qle_pos_l _ _ _ H1 H12); clear H5 H6 H7 H8 H9 H10 H11 H12; repeat rewrite Qmult_zero_right; intros H5 H6 H7 H8 H9 H10 H11 H12; split; left; repeat split. abstract (stepr ((1/2)*((e+f+g+h)+(a+b+c+d))); [|qZ_numerals; field; auto]; apply Qlt_mult_pos_pos; auto; apply Qlt_le_reg_pos; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto). abstract (stepr ((1/2)*((e-f-g+h)+(a-b-c+d))); [|qZ_numerals; field; auto]; apply Qlt_mult_pos_pos; auto; apply Qlt_le_reg_pos; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto). abstract (stepr ((1/2)*((-e-f+g+h)+(-a-b+c+d))); [|qZ_numerals; field; auto]; apply Qlt_mult_pos_pos; auto; apply Qlt_le_reg_pos; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto). abstract (stepr ((1/2)*((-e+f-g+h)+(-a+b-c+d))); [|qZ_numerals; field; auto]; apply Qlt_mult_pos_pos; auto; apply Qlt_le_reg_pos; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto). abstract (stepr ((a+b+c+d)*(Qone+Qone)); trivial; qZ_numerals; field; auto). abstract (stepr ((e+f+g+h)-(a+b+c+d)); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero; trivial). abstract (stepr ((a-b-c+d)*(Qone+Qone)); trivial; qZ_numerals; field; auto). abstract (stepr ((e-f-g+h)-(a-b-c+d)); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero; trivial). abstract (stepr ((-a-b+c+d)*(Qone+Qone)); trivial; qZ_numerals; field; auto). abstract (stepr ((-e-f+g+h)-(-a-b+c+d)); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero; trivial). abstract (stepr ((-a+b-c+d)*(Qone+Qone)); trivial; qZ_numerals; field; auto). abstract (stepr ((-e+f-g+h)-(-a+b-c+d)); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero; trivial). generalize (Qmult_resp_Qle_neg_l _ _ _ H2 H5); generalize (Qmult_resp_Qle_neg_l _ _ _ H2 H6); generalize (Qmult_resp_Qle_neg_l _ _ _ H3 H7); generalize (Qmult_resp_Qle_neg_l _ _ _ H3 H8); generalize (Qmult_resp_Qle_neg_l _ _ _ H4 H9); generalize (Qmult_resp_Qle_neg_l _ _ _ H4 H10); generalize (Qmult_resp_Qle_neg_l _ _ _ H1 H11); generalize (Qmult_resp_Qle_neg_l _ _ _ H1 H12); clear H5 H6 H7 H8 H9 H10 H11 H12; repeat rewrite Qmult_zero_right; intros H5 H6 H7 H8 H9 H10 H11 H12; split; right; repeat split. abstract (stepl (((e+f+g+h)+(a+b+c+d))*(1/2)); [|qZ_numerals; field; auto]; apply Qlt_mult_neg_pos; auto; apply Qlt_le_reg_neg; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto). abstract (stepl (((e-f-g+h)+(a-b-c+d))*(1/2)); [|qZ_numerals; field; auto]; apply Qlt_mult_neg_pos; auto; apply Qlt_le_reg_neg; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto). abstract (stepl (((-e-f+g+h)+(-a-b+c+d))*(1/2)); [|qZ_numerals; field; auto]; apply Qlt_mult_neg_pos; auto; apply Qlt_le_reg_neg; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto). abstract (stepl (((-e+f-g+h)+(-a+b-c+d))*(1/2)); [|qZ_numerals; field; auto]; apply Qlt_mult_neg_pos; auto; apply Qlt_le_reg_neg; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto). abstract (stepl ((a+b+c+d)*(Qone+Qone)); trivial; qZ_numerals; field; auto). abstract (stepl ((e+f+g+h)-(a+b+c+d)); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero_neg; trivial). abstract (stepl ((a-b-c+d)*(Qone+Qone)); trivial; qZ_numerals; field; auto). abstract (stepl ((e-f-g+h)-(a-b-c+d)); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero_neg; trivial). abstract (stepl ((-a-b+c+d)*(Qone+Qone)); trivial; qZ_numerals; field; auto). abstract (stepl ((-e-f+g+h)-(-a-b+c+d)); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero_neg; trivial). abstract (stepl ((-a+b-c+d)*(Qone+Qone)); trivial; qZ_numerals; field; auto). abstract (stepl ((-e+f-g+h)-(-a+b-c+d)); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero_neg; trivial). Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier