Examples of Dependent Types
I think it helps to keep in mind the propositions as types mantra. Every type can be read either as a propostion or a set. This gives us two readings (let's just consider types dependent on natural numbers):


A dependent type $P : \mathtt{nat} \to \mathtt{Type}$ is like a family of sets $P(0), P(1), P(2), \ldots$
A dependent type $P : \mathtt{nat} \to \mathtt{Type}$ is a property of natural numbers where we think of $P(n)$ as the proofs that $n$ has property $P$


With this in mind it may be easier to make sense of dependent types. For instance, consider:


$\mathtt{Mat}(n)$: the type of matrices of size $n \times n$
$\mathtt{Less}(a,b)$: the proofs that $a &lt; b$


Then $\mathtt{Mat}(n)$ should be thought of as a collection of sets, one for each $n$, while $\mathtt{Less}(a,b)$ is a relation (a binary predicate) on pairs $(a,b)$.

Your first three examples (NVec, NMMatrix, Fin) are dependen types of the first kind. The other ones are of the second kind.

Strictly speaking, when you say "a pair of integers where teh second is greater than the first", that is not a dependent type but an element of the dependent sum, i.e,

$$\mathtt{PAIR} = \textstyle\sum_{(a,b) : \mathtt{nat} \times \mathtt{nat}} \mathtt{Less}(a,b),$$

i.e., a triple $(a, b, p)$ where $p$ is a proof that $a &lt; b$. Similarly, your NBtree and SBTree examples are really dependent sums of the form $\sum_{t : \mathtt{Tree}} P(t)$, not dependent types. The sums of course use dependent types $P(t) = \text{"proofs that the tree $t$ is height-balanced"}$ and $P(t) = \text{"proofs that the tree $t$ is sorted"}$.