proposition: Lemma Incl_M_absorbs_Is_refining_M_M:forall mu, Incl_M mu MM -> Is_refining_M (product inv_MM mu).
proof: Proof. intros ((a,b),(c,d)); unfold Incl_M, Is_refining_M, Bounded_M, product, inv_digit, map_digits, inv_MM, fst, snd. replace (0/1 - 1/1) with (Qopp Qone); [|qZ_numerals; field; auto]; replace (1/1 + 0/1) with Qone; [|qZ_numerals; field; auto]; replace (3/1 - 0/1) with (Qone+Qone+Qone); [|qZ_numerals; field; auto]; replace (0/1 + 3/1) with (Qone+Qone+Qone); [|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; intros H3 H4 H5 H6; split; left; repeat split. stepr ((1/3)*(d+c)); [|qZ_numerals; field; auto]; apply Qlt_mult_pos_pos; auto. stepr ((1/3)*(d-c)); [|qZ_numerals; field; auto]; apply Qlt_mult_pos_pos; auto. stepr ((a+b)+(1/3)*(d+c)); [|qZ_numerals; field; auto]; apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone); auto; stepl Zero; trivial; stepr (((a+b)*(Qone+Qone+Qone))-((c + d)*-Qone)); [|qZ_numerals; field; auto];apply Qle_Qminus_Zero; trivial. stepr ((a-b)+(1/3)*(d-c)); [|qZ_numerals; field; auto]; apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone); auto; stepl Zero; trivial; stepr ((d-c)-((b-a)*(Qone+Qone+Qone))); [|qZ_numerals; field; auto];apply Qle_Qminus_Zero; trivial. stepr ((1/3)*(c+d)-(a+b)); [|qZ_numerals; field; auto]; apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone); auto; stepl Zero; trivial; stepr ((c+d)-((a+b)*(Qone+Qone+Qone))); [|qZ_numerals; field; auto];apply Qle_Qminus_Zero; trivial. stepr ((1/3)*(d-c)+(b-a)); [|qZ_numerals; field; auto]; apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone); auto; stepl Zero; trivial; stepr (((b-a)*(Qone+Qone+Qone))-((d-c)*-Qone)); [|qZ_numerals; field; auto];apply Qle_Qminus_Zero; trivial. 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; intros H3 H4 H5 H6; split; right; repeat split. stepl ((d+c)*(1/3)); [|qZ_numerals; field; auto]; apply Qlt_mult_neg_pos; auto. stepl ((d-c)*(1/3)); [|qZ_numerals; field; auto]; apply Qlt_mult_neg_pos; auto. stepl ((a+b)+(1/3)*(d+c)); [|qZ_numerals; field; auto]; apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone); auto; stepr Zero; trivial; stepl (((a+b)*(Qone+Qone+Qone))-((c + d)*-Qone)); [|qZ_numerals; field; auto];apply Qle_Qminus_Zero_neg; trivial. stepl ((a-b)+(1/3)*(d-c)); [|qZ_numerals; field; auto]; apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone); auto; stepr Zero; trivial; stepl ((d-c)-((b-a)*(Qone+Qone+Qone))); [|qZ_numerals; field; auto];apply Qle_Qminus_Zero_neg; trivial. stepl ((1/3)*(c+d)-(a+b)); [|qZ_numerals; field; auto]; apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone); auto; stepr Zero; trivial; stepl ((c+d)-((a+b)*(Qone+Qone+Qone))); [|qZ_numerals; field; auto];apply Qle_Qminus_Zero_neg; trivial. stepl ((1/3)*(d-c)+(b-a)); [|qZ_numerals; field; auto]; apply Qmult_resp_Qle_pos_r with (Qone+Qone+Qone); auto; stepr Zero; trivial; stepl (((b-a)*(Qone+Qone+Qone))-((d-c)*-Qone)); [|qZ_numerals; field; auto];apply Qle_Qminus_Zero_neg; trivial. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M