proposition: Lemma Incl_M_R_unfolded_auxiliary_7: 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)) -> 0 <= (a + b) / (c + d).
proof: Proof. intros a b c d Hdc; destruct (not_Qeq_inf _ _ Hdc); [ apply Incl_M_R_unfolded_auxiliary_72 | apply Incl_M_R_unfolded_auxiliary_71 ]; assumption. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Bounded_M