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