proposition: Lemma iota_Sr i n: iota i n.+1 = rcons (iota i n) (i+n).
proof: Proof. by elim: n i => [i| n H i]; rewrite ? addn0 // /= - addSnnS - H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)