proposition: Lemma presentation_S4 : 'SG_4 \isog Grp ( s0 : s1 : s2 : (s0^+2, s1^+2, s2^+2, s0*s1*s0 = s1*s0*s1, s1*s2*s1 = s2*s1*s2, s0*s2 = s2*s0 ) ).
proof: Proof. have Gen3 (gt : finGroupType) (a b c : gt) : <[a]> <*> <[b]> <*> <[c]> = <<[set a; b; c]>>. by rewrite -!setUA -!joingU1 !joingA. apply intro_isoGrp. - apply/existsP; exists ('s_0, 's_1, 's_2). rewrite /= !xpair_eqE /=; apply/andP; split. + rewrite Gen3 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. do 3 do [apply/andP; split; first by rewrite expgS expg1 eltr2]. do 2 do [apply/andP; split; first by apply/eqP/eltr_braid]. by apply/eqP/eltr_comm. - move=> Gt H; case/existsP => /= [] [[s0 s1] s2] /eqP[<-{H} Hx0 Hx1 Hx2 H010 H121 H02]. rewrite Gen3; apply/homgP. pose fs := fun i => match i with 0 => s0 | 1 => s1 | 2 => s2 | _ => 1 end. have /presentation_Sn_eltr [f Hf] : relat_Sn 3 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 -orbA. apply/imsetP/idP => [[/= x0] | /or3P[] /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. + exists 's_2; rewrite ?setTI ?Hf //. by apply/imsetP => /=; exists (inord 2); rewrite //= inordK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr