proposition: Lemma ctranspP {m} (c : connector m) : reflect ((forall i, (clink c i != i) -> ((clink c i = i.+1 :> nat) \/ (clink c i = i.-1 :> nat))) /\ (forall i, cflip c i = false)) (ctransp c).
proof: Proof. apply: (iffP andP) => [[/forallP Hl /forallP Hf]|[Hl Hf]]. split=> i. by move=> /(implyP (Hl i))/orP[] /eqP->; [left|right]. by rewrite (negPf (Hf i)). split; last by apply/forallP=> i; rewrite Hf. by apply/forallP=> i; apply/implyP => /Hl[]->; rewrite eqxx // orbT. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple