proposition: Theorem thesis_5_6_10: forall mu alpha, Is_refining_M mu -> {n:nat & {d | Incl_M (product_init mu alpha n) d}}.
proof: Proof. intros ((a,b),(c,d)) alpha H_refining. set (det:=a*d-b*c). set (X := Qmax (Qabs(Qone/(c+d))) (Qabs (Qone/(d-c)))). set (q:=3*(2*(Qabs det))*(X*X)). destruct (Q_Archimedean_nat_inf q) as [n Hn]. exists n. assert (H_n_one_pos: Zero < n + 1); [natZ_numerals; qnat_one; natq_zero; natq_S n; natq_S (S n); auto|]. assert (H_refining_prod:=Is_refining_M_product_init _ alpha n H_refining). apply thesis_5_6_9 with H_refining_prod; unfold redundancy. rewrite (diameter_product_init _ _ _ _ _ _ H_refining_prod H_refining). fold det. rewrite <- Qmult_assoc. apply Qle_lt_trans with ((Qabs det)*((2%nat/(n+1%nat))*(X*X))). apply Qle_reg_mult_l_strong; [apply Qabs_nonneg|]. apply Qmult_Qle_compat. apply thesis_5_7_9. unfold X; apply eta_discriminant_twice_majorised with a b; assumption. apply Qle_Qminus_Zero; apply lb_leq_ub_pointwise. apply Qle_mult_nonneg_nonneg; apply Qabs_nonneg. stepl (((2*Qabs det)*(X*X))/(n+1)). apply Qmult_Qdiv_pos. auto. stepl (3*(2*Qabs det)*(X*X)); [|ring]. stepr (n+1); [| qZ_numerals_one; ring]. fold q. apply Qle_lt_trans with n; trivial. rewrite <- Z_to_Qplus; apply Z_to_Qlt; natZ_numerals; rewrite <- inj_plus; apply inj_lt; omega. revert H_n_one_pos; natZ_numerals; intros H_n_one_pos; field; auto. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M