proposition: Lemma clink_rhalf_cleaner_proof m : [forall i : 'I_(m + m), clink_rhalf_cleaner _ (clink_rhalf_cleaner _ i) == i].
proof: Proof. by apply/forallP => i; rewrite !ffunE rev_ordK. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort