proposition: Lemma sup_leEq : forall n : nat, g_ n[<=]sup.
proof: Proof. intros. rewrite -> leEq_def; intro. apply (less_irreflexive_unfolded _ sup). apply (Psup_unfolded1 (g_ n)). red in |- *. exists n. apply eq_reflexive_unfolded. assumption. Qed.
imports: CoRN.reals.Bridges_LUB