fact: Record connector (m : nat):= connector_of { clink : {ffun 'I_m -> 'I_m}; cflip : {ffun 'I_m -> bool}; cfinv : [forall i, clink (clink i) == i]; cflipinv : [forall i, cflip (clink i) == cflip i]}.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple