Require Import ZArith. Require Import List. Open Scope Z_scope. (* 1 : Give a definition in Coq of the following predicates. Unless specifieed, the numbers are supposed to be of type Z , and the lists of type "list Z" *) (* a) the number b is a divisor of a b) the number n is prime c) d is the least prime divisor of n d) the square root of n is rational e) the list l is palindromic f) the list l is sorted. g) the list l represents the decomposition of n into prime factors *) (* 2 : Translate into Coq the following statements. If some statement is incomplete or ambiguous, please make it more precise : h) Every integer has a unique decomposition into prime factors i) any even number is the sum of two primes j) if a list is sorted and palindromic, then it is a repetition of the same number *) (* 3 Specify any function which takes a list of integers and returns a list with the same elements but without duplicates *)