proposition: Lemma bitonic_sorted (s : seq A) : sorted <=%O s -> s \is bitonic.
proof: Proof. move=> sS; apply/existsP; exists (inord 0); rewrite !inordK //= rot0. apply/existsP; exists (inord (size s)); rewrite !inordK //. by rewrite take_size sS /= drop_size. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort