proposition: Lemma rep_ub_auxiliary_L:forall u' r, 0 <= u' + 1 -> 0 < u' + 3 -> -1 <= r -> r <= 0 -> (3 * r + 1) / (- r + 1) <= u' -> r <= (u' - 1) / (u' + 3).
proof: Proof. intros u' 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 ((-r+1)*u'-(3*r+1)); auto; ring. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier