proposition: Lemma low_bound_for_n_element : forall (n : nat) (r : nat -> OF), {l : OF | forall m : nat, m <= n -> l[<]r m}.
proof: Proof. intros. exists (Hum (fun p : nat => [--](r p[^]2)[-]r p[-]Two) n). intros. apply trick'. intros. apply inequality4. intros. apply inequality3. assumption. Qed.
imports: CoRN.reals.Bridges_LUB