proposition: Lemma Incl_M_L_unfolded_auxiliary_3: forall a b c d, c+d <> 0 -> (c + d) * (-1 / 2 - 1 / 2) <= (a + b) * ((2 + 1) / 2 - 1 / 2) -> (a + b) * (1 / 2 + (2 + 1) / 2) <= (c + d) * (1 / 2 + -1 / 2) -> -1 <= (a + b) / (c + d).
proof: Proof. intros a b c d Hdc. replace (1 / 2 + -1 / 2) with 0; [|field;auto]; replace (-1 / 2 - 1 / 2) with (-1); [|field;auto]; replace ((2 + 1) / 2 - 1 / 2) with 1; [|field;auto]; replace (1 / 2 + (2 + 1) / 2) with 2; [|field;auto]; replace ((a+b) * 2) with ((a+b)+(a+b)); [|field;auto]; rewrite Rmult_0_r; rewrite Rmult_1_r; intros H1 H2; stepl ((-1)/1); [|field;auto]; apply Rmult_Rdiv_pos_Rle; auto. assert (H3:0<=c+d). apply Ropp_le_cancel; stepl ((c+d)*(-1));[|ring]; apply Rle_trans with (a+b); trivial; fourier. destruct (Rle_lt_or_eq_dec _ _ H3) as [H4|H4]; trivial; apply False_ind; apply Hdc; auto. stepl ((c + d) * -1); [|ring]; stepr (a+b); [|ring]; trivial. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier