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