proposition: Lemma diameter2_product:forall xi mu_l mu_r H_xi H_prod (H_l:Is_refining_M mu_l) (H_r:Is_refining_M mu_r) Hll Hrl Hlr Hrr, diameter2 (right_product (left_product xi mu_l) mu_r) H_prod (-Qone) (-Qone) Qone Qone min_one_is_in_base_interval_Q min_one_is_in_base_interval_Q one_is_in_base_interval_Q one_is_in_base_interval_Q = diameter2 xi H_xi (as_Moebius_Q mu_l (-Qone)) (as_Moebius_Q mu_r (-Qone)) (as_Moebius_Q mu_l Qone) (as_Moebius_Q mu_r Qone) Hll Hrl Hlr Hrr.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) ((A,B),(C,D)) ((A',B'),(C',D')) H_xi H_prod H_l H_r Hll Hrl Hlr Hrr. assert (H_mul_bound:=proj1 H_l); assert (H_mur_bound:=proj1 H_r); generalize (proj1 H_prod). unfold diameter2, left_product, right_product, as_Tensor_Q, as_Moebius_Q, fst, snd. intros H_pbounded. assert (HCD:=Bounded_M_c_plus_d_nonzero _ _ _ _ H_mul_bound). assert (HCDm:=Bounded_M_d_minus_c_nonzero _ _ _ _ H_mul_bound). assert (HC'D':=Bounded_M_c_plus_d_nonzero _ _ _ _ H_mur_bound). assert (HC'D'm:=Bounded_M_d_minus_c_nonzero _ _ _ _ H_mur_bound). assert (H1p:=Bounded_T_e_mf_mg_h_nonzero _ _ _ _ _ _ _ _ H_pbounded); assert (H2p:=Bounded_T_me_mf_g_h_nonzero _ _ _ _ _ _ _ _ H_pbounded); assert (H3p:=Bounded_T_me_f_mg_h_nonzero _ _ _ _ _ _ _ _ H_pbounded); assert (H4p:=Bounded_T_e_f_g_h_nonzero _ _ _ _ _ _ _ _ H_pbounded). apply (f_equal2 Qminus); [ apply (f_equal4 Qmax4)|apply (f_equal4 Qmin4)]. abstract (field; repeat split; [ring_exact_Q HC'D'm|ring_exact_Q HCDm|ring_exact_Q H1p]). abstract (field; repeat split; [ring_exact_Q HC'D'|ring_exact_Q HCDm|ring_exact_Q H2p]). abstract (field; repeat split; [ring_exact_Q HC'D'm|ring_exact_Q HCD|ring_exact_Q H3p]). abstract (field; repeat split; [ring_exact_Q HC'D'|ring_exact_Q HCD|ring_exact_Q H4p]). abstract (field; repeat split; [ring_exact_Q HC'D'm|ring_exact_Q HCDm|ring_exact_Q H1p]). abstract (field; repeat split; [ring_exact_Q HC'D'|ring_exact_Q HCDm|ring_exact_Q H2p]). abstract (field; repeat split; [ring_exact_Q HC'D'm|ring_exact_Q HCD|ring_exact_Q H3p]). abstract (field; repeat split; [ring_exact_Q HC'D'|ring_exact_Q HCD|ring_exact_Q H4p]). Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M