Tutaj będzie jakaś prosta demonstracja możliwości Coqa.

Kilka prostych funkcji na listach

Sortowanie przez wstawianie (TODO)

Mapowanie funkcji monotonicznej zachowuje porządek