proposition: Lemma Nzorn : forall I:nat -> Prop, (exists n : nat, I n) -> Nbound I -> { n:nat | I n /\ (forall i:nat, I i -> (i <= n)%nat) }.
proof: Proof. intros I H H0; set (E := fun x:R => exists i : nat, I i /\ INR i = x); assert (H1 : bound E). { unfold Nbound in H0; elim H0; intros N H1; unfold bound; exists (INR N); unfold is_upper_bound; intros; unfold E in H2; elim H2; intros; elim H3; intros; rewrite <- H5; apply le_INR; apply H1; assumption. } assert (H2 : exists x : R, E x). { elim H; intros; exists (INR x); unfold E; exists x; split; [ assumption | reflexivity ]. } destruct (completeness E H1 H2) as (x,(H4,H5)); unfold is_upper_bound in H4, H5; assert (H6 : 0 <= x). { destruct H2 as (x0,H6). remember H6 as H7. destruct H7 as (x1,(H8,H9)). apply Rle_trans with x0; [ rewrite <- H9; change (INR 0 <= INR x1); apply le_INR; apply Nat.le_0_l | apply H4; assumption ]. } assert (H7 := archimed x); elim H7; clear H7; intros; assert (H9 : x <= IZR (up x) - 1). { apply H5; intros x0 H9. assert (H10 := H4 _ H9); unfold E in H9; elim H9; intros x1 (H12,<-). apply Rplus_le_reg_l with 1; replace (1 + (IZR (up x) - 1)) with (IZR (up x)); [ idtac | ring ]; replace (1 + INR x1) with (INR (S x1)); [ idtac | rewrite S_INR; ring ]. assert (H14 : (0 <= up x)%Z). { apply le_IZR; apply Rle_trans with x; [ apply H6 | left; assumption ]. } destruct (IZN _ H14) as (x2,H15). rewrite H15, <- INR_IZR_INZ; apply le_INR; apply Nat.le_succ_l. apply INR_lt; apply Rle_lt_trans with x; [ assumption | rewrite INR_IZR_INZ; rewrite <- H15; assumption ]. } assert (H10 : x = IZR (up x) - 1). { apply Rle_antisym; [ assumption | apply Rplus_le_reg_l with (- x + 1); replace (- x + 1 + (IZR (up x) - 1)) with (IZR (up x) - x); [ idtac | ring ]; replace (- x + 1 + x) with 1; [ assumption | ring ] ]. } assert (H11 : (0 <= up x)%Z). { apply le_IZR; apply Rle_trans with x; [ apply H6 | left; assumption ]. } assert (H12 := IZN_var H11); elim H12; clear H12; intros x0 H8; assert (H13 : E x). 2:{ split with (pred x0); unfold E in H13; elim H13; intros; elim H12; intros; rewrite H10 in H15; rewrite H8 in H15; rewrite <- INR_IZR_INZ in H15; assert (H16 : INR x0 = INR x1 + 1). { rewrite H15; ring. } rewrite <- S_INR in H16; assert (H17 := INR_eq _ _ H16); rewrite H17; simpl; split. { assumption. } intros; apply INR_le; rewrite H15; rewrite <- H15; elim H12; intros; rewrite H20; apply H4; unfold E; exists i; split; [ assumption | reflexivity ]. } elim (classic (E x)); intro; try assumption. cut (forall y:R, E y -> y <= x - 1). { intro H13; assert (H14 := H5 _ H13); lra. } intros y H13; assert (H14 := H4 _ H13); elim H14; intro H15; unfold E in H13; elim H13; intros x1 H16; elim H16; intros H17 H18; apply Rplus_le_reg_l with 1. 2:{ rewrite H15 in H13; elim H12; assumption. } replace (1 + (x - 1)) with x; [ idtac | ring ]; rewrite <- H18; replace (1 + INR x1) with (INR (S x1)); [ idtac | rewrite S_INR; ring ]. cut (x = INR (pred x0)). { intro H19; rewrite H19; apply le_INR; apply Nat.le_succ_l; apply INR_lt; rewrite H18; rewrite <- H19; assumption. } rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; rewrite <- (minus_INR _ 1). { apply f_equal; case x0; [ reflexivity | intro; apply Nat.sub_0_r ]. } induction x0 as [|x0 Hrecx0]. { rewrite H8 in H3. rewrite <- INR_IZR_INZ in H3; simpl in H3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 H3)). } apply le_n_S; apply Nat.le_0_l. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra