proposition: Lemma is_isoP : forall p, reflect (is_iso p) (p \in isometries).
proof: Proof. move=> p; apply: (iffP idP) => [|iso_p]; first exact: isometries_iso. move e1: (p c1) (iso_p c1) => k1; move e0: (p c0) (iso_p c0) k1 e1 => k0. case: k0 e0; do 4?[case] => //= ? e0 e2; do 5?[case] => //= ? e1 e3; try by [non_inj p c0 c1 e0 e1 | non_inj p c0 c3 e0 e3]. by is_isoPtac p id1 e0 e1 e2 e3. by is_isoPtac p sd1 e0 e1 e2 e3. by is_isoPtac p sh e0 e1 e2 e3. by is_isoPtac p r1 e0 e1 e2 e3. by is_isoPtac p sd2 e0 e1 e2 e3. by is_isoPtac p r2 e0 e1 e2 e3. by is_isoPtac p r3 e0 e1 e2 e3. by is_isoPtac p sv e0 e1 e2 e3. 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)