I have a type BoundedNat n, representing natural numbers smaller than n. My current implementation is as follows:
Definition BoundedNat n := {x : nat | x < n}.
Manipulating elements of type BoundedNat n is relatively heavyweight. I constantly need to wrap (using exist n ltac:(lia)) and unwrap (using proj1_sig) elements. How can I best piggyback off the underlying type's notations, equality, ordering, etc.?
Though you can definitely roll up your own implementation of bounded natural numbers, I strongly encourage you to reuse an existing one. My favorite library for that is ssreflect. It contains an ordinal n type family that corresponds to your BoundedNat, defined in fintype.v (doc here). There is a coercion from ordinal to nat so that you can readily reuse most operators on natural numbers transparently -- e.g. you can write i < j directly when i j : ordinal n.
Building terms of ordinal is more complicated, since it requires the proof argument. There is no best way of finding this proof, so the way to proceed depends on the application. For instance, adding a constant to a bounded nat is common enough to deserve a specialized operation in ssreflect:
rshift : forall m n, ordinal n -> ordinal (m + n)
One of the advantages of using ssreflect is that it comes with generic support for subset types like ordinal. For instance, there is a insub : nat -> option (ordinal n) function that succeeds if an only if its argument is bounded by n. This function works not only for nat and ordinal, but for any pair of types connected by the subtype interface: sT is a subtype of T if it is of the form {x : T | P x} for some boolean predicate P. Thus, you can manipulate subtypes with a consistent interface rather than rolling up your own each time.