proposition: Lemma spec_sorted_rec a l: spec_sorted (a::l) = (if l== nil then a <=1 else gespec a (head 0 l)) && spec_sorted l.
proof: Proof. case: l; first by rewrite -/(rcons nil a) spec_sorted_rcons andbT //. by move => b l; rewrite /spec_sorted /= andbA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)