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