proposition: Lemma cfun_rhalf_cleaner m (t : (m + m).-tuple A) : cfun (rhalf_cleaner m) t = [tuple match split i with | inl x => min (tnth t i) (tnth t (rshift m (rev_ord x))) | inr x => max (tnth t (lshift m (rev_ord x))) (tnth t i) end | i < m + m].
proof: Proof. apply: eq_from_tnth => i /=. rewrite /rhalf_cleaner /cfun /= !tnth_map /= tnth_ord_tuple !ffunE. case: splitP => [j iE|k iE]; rewrite /= iE. rewrite leq_subRL ?(leq_trans (ltn_ord _)) ?leq_addr //. rewrite leq_add // 1?ltnW //. by congr (min _ (tnth _ _)); apply/val_eqP; rewrite /= iE addnBA. rewrite -addnS subnDl leqNgt ltn_subLR // addSn ltnS addnC -addnA leq_addr /=. rewrite maxC; congr (max (tnth _ _) _). by apply/val_eqP; rewrite /= iE -addnS subnDl. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort