Some lemmata for lists and non-empty lists

[pmbittner]

These are some lemmata we needed in our project Vatras for reasoning on non-empty lists. It seemed these lemmata could be generally useful to other people as well.

-- PR is part of Zurihac 2025

[Taneb]

These look like good additions! Can you update Changelog.md with these?

[pmbittner]

Ok, I updated the changelog as well. :)

[pmbittner]

I also migrated some additional lemmas from Data.List.Properties.

[pmbittner]

Thank you for the review. :) I integrated the requested changes. I also got rid of the rewrite by introducing an analogous lemma to Data.List.Properties and then reusing that.

[pmbittner]

Hi everyone,

I implemented the requested changes. Implementing the length-++-≤ʳ theorem required some additional lemmata, which unfortunately required another theorem (++-identityʳ) which was located below in that file. So I had to reorder some theorems, including module definitions. Please check whether my changes remain idiomatic to the standard library.

(Maybe there is a simpler proof for length-++-≤ʳ but I did not find it yet.)

[MatthewDaggitt]

Thanks @pmbittner for the great contribution and apologies for the delay. Merging them in now.