+definition is_increasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a n ≤ a (S n).
+definition is_decreasing ≝ λO:pordered_set.λa:nat→O.∀n:nat.a (S n) ≤ a n.
+
+definition is_upper_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.a n ≤ u.
+definition is_lower_bound ≝ λO:pordered_set.λa:nat→O.λu:O.∀n:nat.u ≤ a n.
+
+record is_sup (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
+ { sup_upper_bound: is_upper_bound O a u;
+ sup_least_upper_bound: ∀v:O. is_upper_bound O a v → u≤v
+ }.
+
+record is_inf (O:pordered_set) (a:nat→O) (u:O) : Prop ≝
+ { inf_lower_bound: is_lower_bound O a u;
+ inf_greatest_lower_bound: ∀v:O. is_lower_bound O a v → v≤u
+ }.
+
+record is_bounded_below (O:pordered_set) (a:nat→O) : Type ≝
+ { ib_lower_bound: O;
+ ib_lower_bound_is_lower_bound: is_lower_bound ? a ib_lower_bound
+ }.
+
+record is_bounded_above (O:pordered_set) (a:nat→O) : Type ≝
+ { ib_upper_bound: O;
+ ib_upper_bound_is_upper_bound: is_upper_bound ? a ib_upper_bound
+ }.
+
+record is_bounded (O:pordered_set) (a:nat→O) : Type ≝
+ { ib_bounded_below:> is_bounded_below ? a;
+ ib_bounded_above:> is_bounded_above ? a
+ }.
+
+record bounded_below_sequence (O:pordered_set) : Type ≝
+ { bbs_seq:1> nat→O;
+ bbs_is_bounded_below:> is_bounded_below ? bbs_seq
+ }.
+
+record bounded_above_sequence (O:pordered_set) : Type ≝
+ { bas_seq:1> nat→O;
+ bas_is_bounded_above:> is_bounded_above ? bas_seq
+ }.
+
+record bounded_sequence (O:pordered_set) : Type ≝
+ { bs_seq:1> nat → O;
+ bs_is_bounded_below: is_bounded_below ? bs_seq;
+ bs_is_bounded_above: is_bounded_above ? bs_seq
+ }.
+
+definition bounded_below_sequence_of_bounded_sequence ≝
+ λO:pordered_set.λb:bounded_sequence O.
+ mk_bounded_below_sequence ? b (bs_is_bounded_below ? b).
+
+coercion cic:/matita/ordered_sets/bounded_below_sequence_of_bounded_sequence.con.
+
+definition bounded_above_sequence_of_bounded_sequence ≝
+ λO:pordered_set.λb:bounded_sequence O.
+ mk_bounded_above_sequence ? b (bs_is_bounded_above ? b).
+
+coercion cic:/matita/ordered_sets/bounded_above_sequence_of_bounded_sequence.con.
+
+definition lower_bound ≝
+ λO:pordered_set.λb:bounded_below_sequence O.
+ ib_lower_bound ? b (bbs_is_bounded_below ? b).
+
+lemma lower_bound_is_lower_bound:
+ ∀O:pordered_set.∀b:bounded_below_sequence O.
+ is_lower_bound ? b (lower_bound ? b).
+intros; unfold lower_bound; apply ib_lower_bound_is_lower_bound.