proposition: Lemma cfun_rhalf_cleaner_rev n (t : (n + n).-tuple A) : let t1 := cfun (half_cleaner false n) [tuple of ttake t ++ rev (tdrop t)] in cfun (rhalf_cleaner n) t = [tuple of ttake t1 ++ rev (tdrop t1)].
proof: Proof. rewrite /= [LHS]cat_ttake_tdrop; congr [tuple of _ ++ _]. by apply: cfun_rhalf_cleaner_rev_take. by apply: cfun_rhalf_cleaner_rev_drop. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort