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