proposition: Lemma stable : forall x y, x \in dir_iso3 -> y \in dir_iso3 -> x * y \in dir_iso3.
proof: Proof. move=> x y; rewrite !L_iso sop_morph => Hx Hy. by move/sop: y Hy; apply/allP; move/sop: x Hx; 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)