proposition: Lemma rot_eq_c0 : forall r s : {perm square}, is_rot r -> is_rot s -> r c0 = s c0 -> r = s.
proof: Proof. rewrite /is_rot => r s; move/eqP => hr; move/eqP=> hs hrs; apply/permP => a. have ->: a = (r1 ^+ a) c0 by apply/eqP; case: a; do 4?case=> //=; rewrite ?permM !permE. by rewrite -!permM -!commuteX // !permM hrs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)