More lemmas for list's prefix_of and suffix_of

More properties of prefix_of and suffix_of:

• they are partial orders, not just pre orders
• prefix_nil_inv and prefix_of_down_total.