proposition: Lemma tsorted2 (t : 2.-tuple A) : sorted <=%O t = (tnth t ord0 <= tnth t ord_max)%O.
proof: Proof. by case: t => [] [] // a [] // b [] //= i; rewrite !(tnth_nth a) /= andbT. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify)