proposition: Lemma bound_tk2 : forall (n : nat) (g : nat -> OF), (forall m : nat, m <= n -> g m[<]([0]:OF)) -> Hum g n[<][0].
proof: Proof. intros n g H. induction n as [| n Hrecn]. simpl in |- *. apply H. constructor. simpl in |- *. astepr ([0][+]([0]:OF)). apply plus_resp_less_both. apply H. apply le_n. apply Hrecn. intros. apply H. apply Nat.le_trans with (m := n). assumption. apply Nat.le_succ_diag_r. Qed.
imports: CoRN.reals.Bridges_LUB