proposition: Lemma cflip_merge_proof m1 m2 (c1 : connector m1) (c2 : connector m2) : [forall i, cflip_merge c1 c2 (clink_merge c1 c2 i) == cflip_merge c1 c2 i].
proof: Proof. apply/forallP=> i /=. rewrite !ffunE; case: (splitP i) => [j iE|k iE]. by rewrite split_lshift (forallP (cflipinv c1) j). by rewrite split_rshift (forallP (cflipinv c2) k). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple