proposition: Lemma finite_greater : forall N:nat, exists M : R, (forall n:nat, (n <= N)%nat -> Un n <= M).
proof: Proof. intro; induction N as [| N HrecN]. - split with (Un 0); intros. rewrite (proj1 (Nat.le_0_r n) H); apply (Req_le (Un 0) (Un 0) (eq_refl (Un 0))). - elim HrecN; clear HrecN; intros; split with (Rmax (Un (S N)) x); intros; elim (Rmax_Rle (Un (S N)) x (Un n)); intros; clear H1; inversion H0. + rewrite <- H1; rewrite <- H1 in H2; apply (H2 (or_introl (Un n <= x) (Req_le (Un n) (Un n) (eq_refl (Un n))))). + apply (H2 (or_intror (Un n <= Un (S N)) (H n H3))). Qed.
imports: Rbase Rfunctions Compare