proposition: Lemma Incl_M_L_unfolded_auxiliary_1: forall a b c d, d - c <> 0 -> (d - c) * (-1 / 2 - 1 / 2) <= (b - a) * ((2 + 1) / 2 - 1 / 2) -> (b - a) * (1 / 2 + (2 + 1) / 2) <= (d - c) * (1 / 2 + -1 / 2) -> -1 <= (b - a) / (d - c).
proof: Proof. intros a b c d Hdc. assert (Hcd:(c-d)<>0);[apply Rminus_eq_contra; intro; apply Hdc; apply Rminus_diag_eq; auto|]; 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 ((b - a) * 2) with ((b-a)+(b-a)); [|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<=d-c). apply Ropp_le_cancel; stepl ((d-c)*(-1));[|ring]; apply Rle_trans with (b-a); trivial; fourier. destruct (Rle_lt_or_eq_dec _ _ H3) as [H4|H4]; trivial; apply False_ind; apply Hdc; auto. stepl ((d - c) * -1); [|ring]; stepr (b - a); [|ring]; trivial. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier