proposition: Lemma sup_tail_leEq : forall N m : nat, N <= m -> g_ m[<=]sup_tail N.
proof: Proof. intros. unfold sup_tail in |- *. case (le_witness_informative N m H). intro k. intro. apply leEq_wdl with (x := tail_seq g N k). apply sup_leEq. simpl in |- *. rewrite e. apply eq_reflexive_unfolded. Qed.
imports: CoRN.reals.Bridges_LUB