proposition: Lemma maxN : forall (a b:R) (del:posreal), a < b -> { n:nat | a + INR n * del < b /\ b <= a + INR (S n) * del }.
proof: Proof. intros; set (I := fun n:nat => a + INR n * del < b); assert (H0 : exists n : nat, I n). { exists 0%nat; unfold I; rewrite Rmult_0_l; rewrite Rplus_0_r; assumption. } cut (Nbound I). { intro; assert (H2 := Nzorn H0 H1); elim H2; intros x p; exists x; elim p; intros; split. { apply H3. } destruct (total_order_T (a + INR (S x) * del) b) as [[Hlt|Heq]|Hgt]. { assert (H5 := H4 (S x) Hlt); elim (Nat.nle_succ_diag_l _ H5). } { right; symmetry ; assumption. } left; apply Hgt. } assert (H1 : 0 <= (b - a) / del). { unfold Rdiv; apply Rmult_le_pos; [ apply Rge_le; apply Rge_minus; apply Rle_ge; left; apply H | left; apply Rinv_0_lt_compat; apply (cond_pos del) ]. } elim (archimed ((b - a) / del)); intros; assert (H4 : (0 <= up ((b - a) / del))%Z). { apply le_IZR; simpl; left; apply Rle_lt_trans with ((b - a) / del); assumption. } assert (H5 := IZN _ H4); elim H5; clear H5; intros N H5; unfold Nbound; exists N; intros; unfold I in H6; apply INR_le; rewrite H5 in H2; rewrite <- INR_IZR_INZ in H2; left; apply Rle_lt_trans with ((b - a) / del); try assumption; apply Rmult_le_reg_l with (pos del); [ apply (cond_pos del) | unfold Rdiv; rewrite <- (Rmult_comm (/ del)); rewrite <- Rmult_assoc; rewrite Rinv_r; [ rewrite Rmult_1_l; rewrite Rmult_comm; apply Rplus_le_reg_l with a; replace (a + (b - a)) with b; [ left; assumption | ring ] | assert (H7 := cond_pos del); red; intro; rewrite H8 in H7; elim (Rlt_irrefl _ H7) ] ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra