proposition: Lemma tmap_network (n : network m) : {homo f : x y / (x <= y)%O >-> (x <= y)%O} -> {morph tmap f : t / nfun n t >-> nfun n t}.
proof: Proof. by move=> Hm t; elim: n t => //= a n IH t; rewrite -tmap_connector // IH. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple