[SOLVED] CS Homework 10: Predicate for Sorted Lists

Homework 10: Predicate for Sorted Lists

(a)Define a predicateSortas an Idris data type that is truefor lists ofNats that are sorted.Hint 1: Your data type definition needs 3 constructors.Hint 2: You have to reuse theLessdata type in the type ofone of the constructors.
data Less : Nat -> Nat -> Type where Suc : Less n (S n) Trans : Less k n -> Less n m -> Less k m
(b)Express and prove the fact that[3,5]is sorted in Idris.(c)Express and prove the theorem in Idris that the tail ofa sorted list is also sorted.(d)Express and prove the theorem in Idris that the firstelement of a sorted list is smaller than its second element.(e)Express and prove the theorem in Idris that removingthe second element form a sorted list yields a sorted list.