fact: Definition clink_half_cleaner m : {ffun 'I_(m + m) -> 'I_(m + m)} := [ffun i => match split i with | inl x => rshift _ x | inr x => lshift _ x end].
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple nsort