proposition: Lemma mkseq_succ (T: Type) (f: nat -> T) n: mkseq f n.+1 = rcons (mkseq f n) (f n).
proof: Proof. rewrite /mkseq - {3} (add0n n). by elim: n (0) => [n |n H m]; rewrite ? addn0 //= addnS - addSn - H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)