proposition: Lemma L_less_sup_n : forall n : nat, L[<=]sup_tail n.
proof: Proof. intros. unfold L in |- *. change (inf sup_tail_as_Cauchy[<=]CS_seq OF sup_tail_as_Cauchy n) in |- *. apply inf_geEq. Qed.
imports: CoRN.reals.Bridges_LUB