proposition: Lemma cflip_swap_proof (i j : 'I_m) : [forall k, cflip_swap i j (clink_swap i j k) == cflip_swap i j k].
proof: Proof. apply/forallP => /= x. rewrite !ffunE; case: (x =P i) => [|/eqP xDi]. by rewrite eqxx if_same eqxx. case: (x =P j) => [|/eqP xDj]; first by rewrite !eqxx. by rewrite (negPf xDi) (negPf xDj). Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple