proposition: Lemma Incl_M_L_unfolded_auxiliary_72: forall (a b c d:Q), d+c<0 -> (d+c)*((c+d)*(-1/2-1/2))<=(d+c)*((a+b)*((2+1)/2-1/2)) -> -1 <= (a + b) / (c + d).
proof: Proof. intros a b c d Hdc H0; generalize (Qmult_resp_Qle_neg_l _ _ _ Hdc H0); clear H0; replace (-1/2 - 1/2) with (Qopp Qone); [|qZ_numerals; field; auto]; replace ((2+1)/2 - 1/2) with Qone; [|qZ_numerals; field; auto]; intros H_mult; assert (Hcd:c+d<Zero);[ring_exact_Q Hdc|]; apply Qmult_neg_Qle_Qdiv; trivial; ring_exact_Q H_mult. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Bounded_M