proposition: Lemma presentation_S3 : 'SG_3 \isog Grp ( s0 : s1 : (s0^+2 = s1^+2 = 1, s0*s1*s0 = s1*s0*s1) ).
proof: Proof. apply intro_isoGrp. - apply/existsP; exists ('s_0, 's_1). rewrite /= !xpair_eqE; apply/and4P; split; try by rewrite expgS expg1 eltr2. + rewrite joingU1 eqEsubset subsetT /=; apply/subsetP => /= s _. rewrite -(canwordP s). elim: (canword s) => [| t0 t IHt] /=; first by rewrite big_nil group1. rewrite big_cons; apply groupM; last exact: IHt. apply (subsetP (subset_gen _)); rewrite !inE. by case: t0 => [] [| [| //=]] /= _; rewrite eq_refl /= ?orbT. + by apply/eqP/eltr_braid. - move=> Gt H; case/existsP => /= [] [s0 s1] /eqP[<-{H} Hx0 Hx1 H3]. rewrite joingU1; apply/homgP. pose fs := fun i => match i with 0 => s0 | 1 => s1 | _ => 1 end. have /presentation_Sn_eltr [f Hf] : relat_Sn 2 fs. constructor; try by case=> [|[|i]]. by case=> [|i] j // /andP[/leq_ltn_trans /[apply]]. exists f; rewrite {3}eltr_genSn morphim_gen; last exact: subsetT. congr <<_>>; apply/setP => x; rewrite !inE. apply/imsetP/idP => [[/= x0] | /orP[] /eqP ->{x}] /=; rewrite setTI. + move=> /imsetP[/= i _ -> ->]. by case: i => [[|[|i]] //= ] _; rewrite Hf // eq_refl ?orbT. + exists 's_0; rewrite ?setTI ?Hf //. by apply/imsetP => /=; exists (inord 0); rewrite //= inordK. + exists 's_1; rewrite ?setTI ?Hf //. by apply/imsetP => /=; exists (inord 1); rewrite //= inordK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr