proposition: Lemma ndir_s0p : forall p, p \in dir_iso3 -> s0 * p \notin dir_iso3.
proof: Proof. move=> p; rewrite !L_iso sop_morph seqs1. by move/sop: p; apply/allP; vm_compute. 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)