proposition: Lemma leqt_nfun m (n : network m) : ntransp n -> {homo (nfun n : m.-tuple A -> m.-tuple A) : i j / leqt i j}.
proof: Proof. elim: n => /= [_| c n IH /andP[cT nT]] t1 t2 t1Lt2 //=. by apply: IH => //; apply: leqt_cfun. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple