proposition: Theorem up_bound_for_n_element : forall (n : nat) (r : nat -> OF), {b : OF | forall m : nat, m <= n -> r m[<]b}.
proof: Proof. intros. exists (Hum (fun p : nat => r p[^]2[-]r p[+]Two) n). intros. apply trick. intros. apply inequality2. intros. apply inequality1. assumption. Qed.
imports: CoRN.reals.Bridges_LUB