proposition: Lemma leqt_nsorted m (x1 x2 : A) (t : m.-tuple A) (n : network m) : x1 != x2 -> ntransp n -> sorted (>%O) t -> sorted (<=%O) (nfun n t) -> n \is sorting.
proof: Proof. move=> x1Dx2 nT tS tS1; apply: sorted_sorting x1Dx2 _ => t1. suff : forall a b, a <= b < size (nfun n t1) -> (nth x1 (nfun n t1) a <= nth x1 (nfun n t1) b)%O. elim: tval => // y1 [|y2 l] // IH H. rewrite /= (H 0 1) //=. apply: IH => a b /= /andP[aLb bLs]. by apply: (H a.+1 b.+1); rewrite /= !ltnS //= aLb -ltnS. rewrite size_tuple => a b /andP[aLb bLs]. have aLs : a < m by apply: leq_ltn_trans aLb _. pose a1 := Ordinal aLs; pose b1 := Ordinal bLs. have /leqtP/(_ a1 b1 aLb) : leqt (nfun n t) (nfun n t1). apply: leqt_nfun => //. by apply: leqt_sorted. rewrite !(tnth_nth x1); apply. by apply: (sorted_leq_nth le_trans le_refl x1 tS1); rewrite ?(inE, size_tuple). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple