proposition: Lemma card_iso2 : #|isometries2| = 2.
proof: Proof. by rewrite cards2 diff_id_sh. 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)