proposition: Lemma bitonic_rev (s : seq A) : (rev s \is bitonic) = (s \is bitonic).
proof: Proof. suff {s}Hi (s : seq A) : s \is bitonic -> rev s \is bitonic. apply/idP/idP=> [H|]; last by apply: Hi. by rewrite -[s]revK; apply: Hi. move=> /existsP[/= r /existsP[n /andP[tS dS]]]. apply/existsP; rewrite size_rev. have xO : size s - r < (size s).+1 by rewrite ltnS leq_subr. exists (Ordinal xO) => /=. have yO : size s - n < (size s).+1 by rewrite ltnS leq_subr. apply/existsP; exists (Ordinal yO) => /=. rewrite -rev_rotr take_rev drop_rev !rev_sorted size_rotr /rotr. by rewrite !subnA ?subnn -1?ltnS // dS. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort