proposition: Lemma sop_inj : injective sop.
proof: Proof. by move=> p1 p2 /val_inj/(can_inj fgraphK)/val_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)