proposition: Lemma spec_sorted_sorted l: spec_sorted l -> sorted gtn l.
proof: Proof. move /andP => [h _]; move:h. case: l => //= n s; elim: s n => //= m s IHs n /andP [ h /IHs ->]. rewrite andbT;case/orP: h => /eqP -> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)