proposition: Lemma iota_S a n: iota a.+1 n = succ_seq (iota a n).
proof: Proof. by elim: n a => // k H m /=; rewrite H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)