proposition: Lemma nfun_const (a : A) n : nfun n [tuple of nseq m a] = [tuple of nseq m a].
proof: Proof. by elim: n => //= n p IH; rewrite cfun_const IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple