proposition: Lemma limit_lub f x y: limit_of f x -> (forall n, f n <= y) -> T1nf y -> x <= y.
proof: Proof. move => [pa [pb pc] pd ] hy; case (T1ltP y x) => // ha hb. move: (pc _ hb ha) => [n ny]. by move: (T1le_lt_trans ny (pa _ _ (ltnSn n))); rewrite T1ltNge (hy n.+1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)