proposition: Lemma is_iso3P : forall p, reflect (is_iso3 p) (p \in iso3).
proof: Proof. move=> p; apply: (iffP idP); rewrite inE /iso3 /is_iso3b /is_iso3 => e. by move=> fi; rewrite -!permM (eqP e). by apply/eqP; apply/permP=> z; rewrite !permM (e z). 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)