proposition: Lemma clink_eomerge_proof m (c1 : connector m) (c2 : connector m) : [forall i, (clink_eomerge c1 c2 (clink_eomerge c1 c2 i)) == i].
proof: Proof. apply/forallP=> i /=. rewrite !ffunE /=; have [iO|iE] := boolP (odd i). rewrite oliftK val_olift /= odd_double /= (eqP (forallP (cfinv c2) _)). by rewrite idiv2K_odd. rewrite eliftK val_elift /= odd_double /= (eqP (forallP (cfinv c1) _)). by rewrite idiv2K_even. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple