proposition: Lemma rep_lb_auxiliary_L:forall l' r, 0 <= l' + 1 -> 0 < l' + 3 -> -1 <= r -> r <= 0 -> l' <= (3 * r + 1) / (- r + 1) -> (l' - 1) / (l' + 3) <= r.
proof: Proof. intros l' r H1 H2 Hr1 Hr2 IH. apply Rle_zero_Rminus. generalize (Rle_Rminus_zero _ _ IH); clear IH. rewrite Rminus_Rdiv_Rmult; try (solve [apply Rlt_not_eq ; fourier| apply Rlt_not_eq' ; fourier]). rewrite Rdiv_Rminus_Rmult; try (solve [apply Rlt_not_eq ; fourier| apply Rlt_not_eq' ; fourier]). intro IH. assert (Hr3:0< -r+1); [fourier|]. generalize (Rle_pos_nonneg_Rdiv _ _ Hr3 IH); clear IH; intro IH. unfold Rdiv; apply Rle_mult_inv_pos; try fourier. stepr (3*r+1-(-r+1)*l'); auto; ring. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier