proposition: Lemma mkseq_uniqP (f : nat -> T) n : reflect {in gtn n &, injective f} (uniq (mkseq f n)).
proof: Proof. apply: (equivP (uniqP (f 0))); rewrite size_mkseq. by split=> injf i j lti ltj; have:= injf i j lti ltj; rewrite !nth_mkseq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)