proposition: Lemma iota_rem2_spec_sorted j i: spec_sorted (rev (rem i.+2 (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 => //. elim: j 0 i; first by move => n k /=; case (n == k). move => j H i k /=; case: (i==k); first by apply:iota_rem_lespec_sorted. simpl; case ww:(i == k.+2); first by apply:iota_rem_lespec_sorted. move: (H i.+1 k); clear; case: j => // j /=. case wwb: (i.+1 == k). have wwc: k == k.+1 = false by apply/negP => /eqP; exact: n_Sn. by case:j => // j /=; rewrite eqSS (eqP wwb) wwc /= (eqP wwb) eqxx orbT. rewrite /= eqSS; case wwc: (i == k.+1); last by rewrite /= eqxx. rewrite (eqP wwc);case: j => // j /=. by rewrite gtn_eqF /= ?eqxx ?orbT // ltnS - addn2 leq_addr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)