fact: Definition clink_merge m1 m2 (c1 : connector m1) (c2 : connector m2) := [ffun i => match split i with | inl x => lshift _ (clink c1 x) | inr x => rshift _ (clink c2 x) end].
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple