proposition: Lemma iota_rem_lespec_sorted i j n: sorted lespec (rem j (iota i n)).
proof: Proof. elim: n i j; first by move => n k /=; case (n == k). move => j H i k /=; case: (i==k); first by apply: iota_lespec_sorted. move: (H i.+1 k);case j => // j1 /=; case:(i.+1 == k) => //; case: j1 => // j2 /=; rewrite eqxx // orbT //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)