proposition: Lemma cfun_batcher_merge n (t : n.-tuple A) : cfun batcher_merge t = [tuple if odd i then min (tnth t i) (tnth t (inext i)) else max (tnth t i) (tnth t (ipred i)) | i < n].
proof: Proof. rewrite [LHS]cfun_odd_jump //. apply/val_eqP/eqP=> /=; apply/eq_map => i; congr (if _ then min (tnth _ _) (tnth _ _) else max _ _). case: (n) i => //= n1 i; rewrite add1n. by have := ltn_ord i; rewrite ltnS; case: (ltngtP i n1). congr (tnth _ _); apply/val_eqP/eqP=> /=. rewrite /isub /ipred. by case: (n) i => //= n1 i; case: (i : nat) => [|i1]; rewrite ?addn1 ?subn1. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort