proposition: Lemma cfun_half_cleaner b m (t : (m + m).-tuple A) : cfun (half_cleaner b m) t = [tuple match split i with | inl x => (if b then max else min) (tnth t i) (tnth t (rshift m x)) | inr x => (if b then min else max) (tnth t i) (tnth t (lshift m x)) end | i < m + m].
proof: Proof. apply: eq_from_tnth => i /=. rewrite /half_cleaner /cfun /=. rewrite !tnth_map /= !tnth_ord_tuple !ffunE. case: splitP => /= [j iE|k iE]; first by rewrite iE leq_addl; case: b. rewrite ifN; first by case: b. by rewrite -ltnNge (leq_trans (ltn_ord _) _) // iE leq_addr. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort