proposition: Lemma diameter_product:forall mu mu' H_mu H_mu', diameter (product mu mu') (Is_refining_M_product _ _ H_mu H_mu') = (Qabs (Determinant mu))* (diameter mu' H_mu') * (Qabs(as_Moebius_Q (eta_discriminant mu) (as_Moebius_Q mu' (-Qone)))*Qabs(as_Moebius_Q (eta_discriminant mu) (as_Moebius_Q mu' Qone))).
proof: Proof. intros ((a,b),(c,d)) ((a',b'),(c',d')) H_mu H_mu'. assert (H_mu_bound:=proj1 H_mu); assert (H_mu'_bound:=proj1 H_mu'). assert (H_prod:=Is_refining_M_product _ _ H_mu H_mu'); generalize (proj1 H_prod). revert H_prod; unfold diameter, Determinant, eta_discriminant, product, as_Moebius_Q, fst, snd. intros H_prod H_prod_bound. assert (H_cd:=Bounded_M_c_plus_d_nonzero _ _ _ _ H_mu_bound). assert (H_dc:=Bounded_M_d_minus_c_nonzero _ _ _ _ H_mu_bound). assert (H_cd':=Bounded_M_c_plus_d_nonzero _ _ _ _ H_mu'_bound). assert (H_dc':=Bounded_M_d_minus_c_nonzero _ _ _ _ H_mu'_bound). assert (H_pord_denom_one:=Bounded_M_c_plus_d_nonzero _ _ _ _ H_prod_bound). assert (H_prod_denom_min_one:=Bounded_M_d_minus_c_nonzero _ _ _ _ H_prod_bound). assert (H_cd_:c * - Qone + d<>Zero); [ring_exact_Q H_dc|]. assert (H_cd'_:c' * - Qone + d'<>Zero); [ring_exact_Q H_dc'|]. assert (H_prod_denom_min_one_:(c*a'+d*c')* - Qone + (c*b'+d*d') <> Zero); [ring_exact_Q H_prod_denom_min_one|]. qZ_numerals. repeat rewrite <- Qabs_Qmult. repeat rewrite Qminus_Qdiv; trivial. apply (f_equal Qabs). field; repeat split; auto. ring_exact_Q H_pord_denom_one. ring_exact_Q H_prod_denom_min_one. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M