proposition: Lemma cfun_rhalf_cleaner_rev_drop m (t : (m + m).-tuple A) : tdrop (cfun (rhalf_cleaner m) t) = trev (tdrop (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) := rshift _ i; pose a := tnth t k. rewrite !(tnth_nth a) nth_rev; last first. by rewrite tdropE size_drop size_tuple addnK. rewrite !tdropE !nth_drop !(nth_map k) //; last first. - by rewrite size_tuple ltn_add2l. - by rewrite -fintype.enumT fintype.size_enum_ord ltn_add2l. - by rewrite size_drop !size_tuple; have := ltn_ord i; lia. - rewrite size_drop !size_tuple -fintype.enumT fintype.size_enum_ord. by have := ltn_ord i; lia. have -> : m + i = k :> nat by []. rewrite -fintype.enumT fintype.nth_ord_enum. case: splitP => [j kE|j kE]. by have := ltn_ord j; rewrite -kE /= ltnNge leq_addr. rewrite size_drop size_tuple addnK. have -> : m + (m - i.+1) = rshift m (rev_ord i) by []. rewrite fintype.nth_ord_enum. case: splitP => /= [l lE | l lE]; first by have := ltn_ord l; lia. rewrite maxC. congr max. rewrite !(tnth_nth a) nth_cat /= st lE ltnNge leq_addr /=. rewrite nth_rev; last by rewrite sd; have := ltn_ord i; lia. rewrite tdropE nth_drop // size_drop size_tuple addnK. congr nth. have : m + i = m + j by rewrite -kE. by have := ltn_ord i; lia. rewrite !(tnth_nth a) nth_cat /= st ltn_ord. rewrite ttakeE nth_take //; congr nth. have : m + i = m + j by rewrite -kE. by have := ltn_ord i; lia. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort