proposition: Lemma iota_rem_spec_sorted j i: spec_sorted (rev (rem i (iota 0 j))).
proof: Proof. rewrite spec_sorted_rev; apply/andP; split;last first. case:j => // j /=;case ww: (0 == i) => //; case:j => //. by apply: iota_rem_lespec_sorted. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)