proposition: Lemma mkseq_uniq (f: nat -> nat) a n: injective f -> uniq [seq (f i) | i <- iota a n].
proof: Proof. move => h; rewrite (map_inj_uniq h); exact: iota_uniq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)