proposition: Lemma sd1_inv : sd1^-1 = sd1.
proof: Proof. apply: (mulIg sd1); rewrite mulVg; apply/permP. by case; do 4?case=> //=; move=> H; rewrite !permE /= !permE; apply/eqP. 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)