proposition: Lemma clink_half_cleaner_proof m : [forall i : 'I_(m + m), clink_half_cleaner _ (clink_half_cleaner _ i) == i].
proof: Proof. apply/forallP => i; rewrite !ffunE; case: (splitP i) => [j iE|k iE]. by rewrite split_rshift; apply/eqP/val_eqP/eqP. by rewrite split_lshift; apply/eqP/val_eqP/eqP. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort