proposition: Lemma cfun_const (a : A) c : cfun c [tuple of nseq m a] = [tuple of nseq m a].
proof: Proof. apply: eq_from_tnth => /= i. by rewrite tnth_map /= !(tnth_nth a) /= !nth_nseq !if_same maxxx. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple