proposition: Lemma L_iso : forall p, (p \in dir_iso3) = (sop p \in seq_iso_L).
proof: Proof. by move=> p; rewrite (eqP Lcorrect) mem_map ?iso0_1 //; apply: sop_inj. 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)