fact: Definition cflip_eomerge m (c1 : connector m) (c2 : connector m) := [ffun i : 'I_(m + m) => if odd i then cflip c2 (idiv2 i) else cflip c1 (idiv2 i)].
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple