proposition: Lemma Incl_M_absorbs_Is_refining_M_L:forall mu, Incl_M mu LL -> Is_refining_M (product inv_LL mu).
proof: Proof. intros ((a,b),(c,d)); unfold Incl_M, Is_refining_M, Bounded_M, product, inv_digit, map_digits, inv_LL, fst, snd. replace ((-1)/2 - 1/2) with (Qopp Qone); [|qZ_numerals; field; auto]; replace (1/2 + 3/2) with (Qone +Qone); [|qZ_numerals; field; auto]; replace (3/2 - 1/2) with Qone; [|qZ_numerals; field; auto]; replace (1/2 + -1/2) with Zero; [|qZ_numerals; field; auto]; repeat rewrite Qmult_one_right; intros [[[H1 H2]|[H1 H2]] [H3 [H4 [H5 H6]]]]. generalize (Qmult_resp_Qle_pos_l _ _ _ H1 H5); generalize (Qmult_resp_Qle_pos_l _ _ _ H1 H6); generalize (Qmult_resp_Qle_pos_l _ _ _ H2 H3); generalize (Qmult_resp_Qle_pos_l _ _ _ H2 H4); clear H3 H4 H5 H6; repeat rewrite Qmult_zero_right; intros H3 H4 H5 H6; split; left; repeat split. stepr ((1/2)*((d+c)-(a+b))); [|qZ_numerals; field; auto]; apply Qlt_mult_pos_pos; auto; apply Qlt_Qminus_Zero; apply Qle_lt_trans with Zero; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto. stepr ((1/2)*((d-c)-(b-a))); [|qZ_numerals; field; auto]; apply Qlt_mult_pos_pos; auto; apply Qlt_Qminus_Zero; apply Qle_lt_trans with Zero; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto. stepr ((c+d)+(a+b)); [|qZ_numerals; field; auto]; stepl ((c+d)+(c + d)*(Qopp Qone)); [|ring]; apply Qle_plus_plus; auto. stepr (Zero-((b-a)*(Qone+Qone))); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero; trivial. stepr (Zero-((a+b)*(Qone+Qone))); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero; trivial. stepr ((d-c)+(b-a)); [|qZ_numerals; field; auto]; stepl ((d-c)+(d-c)*(Qopp Qone)); [|ring]; apply Qle_plus_plus; auto. generalize (Qmult_resp_Qle_neg_l _ _ _ H1 H5); generalize (Qmult_resp_Qle_neg_l _ _ _ H1 H6); generalize (Qmult_resp_Qle_neg_l _ _ _ H2 H3); generalize (Qmult_resp_Qle_neg_l _ _ _ H2 H4); clear H3 H4 H5 H6; repeat rewrite Qmult_zero_right; intros H3 H4 H5 H6; split; right; repeat split. stepl (((d+c)-(a+b))*(1/2)); [|qZ_numerals; field; auto]; apply Qlt_mult_neg_pos; auto; apply Qlt_Qminus_Zero_neg; apply Qlt_le_trans with Zero; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto. stepl (((d-c)-(b-a))*(1/2)); [|qZ_numerals; field; auto]; apply Qlt_mult_neg_pos; auto; apply Qlt_Qminus_Zero_neg; apply Qlt_le_trans with Zero; trivial; apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto. stepl ((c+d)+(a+b)); [|qZ_numerals; field; auto]; stepr ((c+d)+(c + d)*(Qopp Qone)); [|ring]; apply Qle_plus_plus; auto. stepl (Zero-((b-a)*(Qone+Qone))); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero_neg; trivial. stepl (Zero-((a+b)*(Qone+Qone))); [|qZ_numerals; field; auto]; apply Qle_Qminus_Zero_neg; trivial. stepl ((d-c)+(b-a)); [|qZ_numerals; field; auto]; stepr ((d-c)+(d-c)*(Qopp Qone)); [|ring]; apply Qle_plus_plus; auto. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M