proposition: Lemma val_tmap t : tmap t = map f t :> seq B.
proof: Proof. have -> : tmap t = [tuple of [seq f (tnth t i) | i <- ord_tuple m]]. by apply: eq_from_tnth => i; rewrite !(tnth_map, tnth_ord_tuple). congr tval. by apply: eq_from_tnth => i; rewrite !(tnth_map, tnth_ord_tuple). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)