proposition: Lemma spec_sorted_rev l: (spec_sorted (rev l)) = sorted lespec l && lespec 0 (head 0 l).+1.
proof: Proof. by rewrite /spec_sorted rev_sorted - (head_rev 0 (rev l)) revK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)