proposition: Lemma presentation_S2 : 'SG_2 \isog Grp ( s0 : s0^+2 ).
proof: Proof. apply intro_isoGrp. - apply/existsP; exists ('s_0). rewrite /= !xpair_eqE; apply/andP; split; try by rewrite expgS expg1 eltr2. rewrite 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 => [] [| //=] /= _. - move=> Gt H; case/existsP => /= s0 /eqP[<-{H} Hx0]. apply/homgP. pose fs := fun i => match i with 0 => s0 | _ => 1 end. have /presentation_Sn_eltr [f Hf] : relat_Sn 1 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/eqP => [[/= x0]| ->{x}] /=; rewrite setTI. + move=> /imsetP[/= i _ -> ->]. by case: i => [[|i] //= ] _; rewrite Hf. + exists 's_0; rewrite ?setTI ?Hf //. by apply/imsetP => /=; exists (inord 0); rewrite //= inordK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr