fact: Definition isometries := [set p | [|| p == 1, p == r1, p == r2, p == r3, p == sh, p == sv, p == sd1 | p == sd2 ]].
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)