Miscellaneous theorems
Includes proofs that the rank, length of right spine, and length of the shortest path to an empty node are all equal. We also prove that the rank and size of a tree are always natp, as this is helpful in a later theorem.