proposition: Lemma cfun_rhalf_cleaner_rev_take m (t : (m + m).-tuple A) : ttake (cfun (rhalf_cleaner m) t) = ttake (cfun (half_cleaner false m) [tuple of ttake t ++ rev (tdrop t)]).
proof: Proof. rewrite cfun_rhalf_cleaner cfun_half_cleaner. apply: eq_from_tnth => i /=. have st : size (ttake t) = m. rewrite ttakeE size_take size_tuple. by case: (m) => // n1; rewrite addSn ltnS addnS ltnS leq_addr. have sd : size (tdrop t) = m. by rewrite tdropE size_drop size_tuple addnK. pose k : 'I_(m + m) := lshift _ i; pose a := tnth t k. rewrite !(tnth_nth a) !ttakeE !nth_take //=. rewrite !(nth_map k) //; last first. - by rewrite fintype.size_enum_ord (leq_trans (ltn_ord _) (leq_addr _ _)). - by rewrite fintype.size_enum_ord (leq_trans (ltn_ord _) (leq_addr _ _)). - by rewrite -fintype.enumT fintype.size_enum_ord (leq_trans (ltn_ord _) (leq_addr _ _)). have -> : i = k :> nat by []. rewrite -fintype.enumT fintype.nth_ord_enum. case: splitP => [j kE|j kE]; last first. by have := ltn_ord i; rewrite [i : nat]kE ltnNge leq_addr. congr min. by rewrite !(tnth_nth a) nth_cat /= st ltn_ord ttakeE nth_take. rewrite !(tnth_nth a) nth_cat /= st ifN; last by rewrite -leqNgt leq_addr. rewrite nth_rev; last by rewrite sd addnC addnK. rewrite sd tdropE nth_drop //. by congr nth; lia. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort