proposition: Lemma sorted_batcher_merge (m : nat) (t : (m + m).-tuple bool) : noF (totake t) <= noF (tetake t) <= (noF (totake t)).+2 -> sorted <=%O (tetake t) -> sorted <=%O (totake t) -> sorted <=%O (cfun batcher_merge t).
proof: Proof. move=> /andP[FotLFet FotLFet2] eS oS. pose i := noF (tetake t) - noF (totake t). have i_le2 : i <= 2 by rewrite leq_subLR addn2. have nFE : noF (tetake t) = noF (totake t) + i by rewrite addnC subnK. have [ceS coF ncFE] := sorted_odd_jump (isT : odd 1) i_le2 eS oS nFE. apply: sorted_tetake_totake => //. rewrite ncFE leq_addr -[X in _ <= X]addn1 leq_add2l /=. by rewrite leq_subLR addnC -leq_subLR -addnn leq_addr. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort