proposition: Lemma bitonic_cat (s1 s2 : seq A) : sorted <=%O s1 -> sorted >=%O s2 -> (s1 ++ s2) \is bitonic.
proof: Proof. move=> s1S s2S. apply/existsP; exists (inord 0); rewrite inordK ?rot0 //=. apply/existsP; rewrite size_cat /=. have sLs : size s1 < (size s1 + size s2).+1 by rewrite ltnS leq_addr. exists (Ordinal sLs) => /=. rewrite take_cat ltnn subnn take0 cats0 s1S /=. by rewrite drop_cat ltnn subnn drop0. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort