include "datatypes/constructors.ma".
include "nat/plus.ma".
-include "nat_ordered_set.ma".
-include "sequence.ma".
+include "dama/nat_ordered_set.ma".
+include "dama/sequence.ma".
(* Definition 2.4 *)
definition upper_bound ≝
interpretation "trans_decreasing" 'trans_decreasing = (h_trans_increasing (os_r _)).
lemma hint_nat :
- Type_of_ordered_set nat_ordered_set →
+ Type_OF_ordered_set nat_ordered_set →
hos_carr (os_l (nat_ordered_set)).
intros; assumption;
qed.