proposition: Lemma Incl_M_L_unfolded_auxiliary_8: forall (a b c d:Q), d - c <> 0 -> (d-c)*((b-a)*(1/2+(2+1)/2))<=(d-c)*((d-c)*(1/2+-1/2)) -> (b - a) / (d - c)<=0.
proof: Proof. intros a b c d Hdc. destruct (not_Qeq_inf _ _ Hdc); [ apply Incl_M_L_unfolded_auxiliary_82 | apply Incl_M_L_unfolded_auxiliary_81 ]; assumption. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Bounded_M