proposition: Lemma sorted_sorting n (x1 x2 : A) : x1 != x2 -> (forall t : m.-tuple A, sorted <=%O (nfun n t)) -> n \is sorting.
proof: Proof. wlog x1Lx2 : x1 x2 / (x1 < x2)%O => [Hgs x1Dx2 Hs|]. case: (ltgtP x1 x2) => [/Hgs->|/Hgs->|] //; first by rewrite eq_sym. by move/eqP; rewrite (negPf x1Dx2). move=> x1Dx2 Hgs; apply/forallP => /= t. pose f x := if x then x2 else x1. pose g x := if (x <= x1)%O then false else true. have fK : cancel f g by case => /=; rewrite /g ?le_refl // leNgt x1Lx2. have gM : {homo g : x y / (x <= y)%O >-> (x <= y)%O}. move=> i j; rewrite /g. case: (leP i x1); case: (leP j x1) => // jLx1 x1Li. by rewrite leNgt (le_lt_trans jLx1). have -> : t = tmap g (tmap f t). by apply: eq_from_tnth => i; rewrite !tnth_map !tnth_ord_tuple fK. by rewrite -tmap_network // val_tmap (homo_sorted gM _ _). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple