proposition: Lemma dir_s0p : forall p, (s0 * p) \in dir_iso3 -> p \notin dir_iso3.
proof: Proof. move=> p Hs0p; move: (ndir_s0p Hs0p); rewrite mulgA. have e: (s0^-1=s0) by inv_tac. by rewrite -{1}e mulVg mul1g. 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)