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