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