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