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