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