proposition: Lemma eta_discriminant_twice_majorised: forall a b c d alpha n, Is_refining_M ((a,b),(c,d)) -> let X := Qmax (Qabs(Qone/(c+d))) (Qabs (Qone/(d-c))) in (Qabs (as_Moebius_Q ((0/1,1/1),(c,d)) (lb alpha n)) * Qabs (as_Moebius_Q ((0/1,1/1),(c,d)) (ub alpha n)))<= X * X.
proof: Proof. intros a b c d alpha n [H_bounded _] X. apply Qmult_Qle_compat ; [| |apply Qabs_nonneg|apply Qabs_nonneg]; subst X; apply maximum_eta_discriminant_base_interval with a b; trivial. apply lb_is_in_base_interval_low. apply lb_is_in_base_interval_up. apply ub_is_in_base_interval_low. apply ub_is_in_base_interval_up. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M