proposition: Theorem presentation_Sn_eltr : relat_Sn -> exists f : {morphism 'SG_n.+1 >-> gT}, forall i, i < n -> f 's_i = 'g_i.
proof: Proof. Proof using. move=> [Hsq Hbraid Hcom]. pose morph_eltr_fun (s : 'S_n.+1) := \prod_(i <- canword s) 'g_i. have morph_eltrP : {morph morph_eltr_fun : x y / x * y}. move=> i j. have:= braidred_to_canword (canword i ++ canword j) => [[redpath [Hpath]]]. rewrite big_cat /= !canwordP /morph_eltr_fun -big_cat /= => Hlast. elim: redpath (_ ++ _) Hpath Hlast => [c _ <- //|] w0 wp IHwp /= c /andP[Hbr] {}/IHwp /[apply] ->. move: Hbr => /orP[]. - rewrite braid_sym; move: c; apply: gencongr_ind => //. move=> a b1 c b2 ->{w0} Hbr; rewrite !big_cat /=; congr (_ * (_ * _)) => {a c}. move: Hbr; rewrite /= mem_cat => /orP[]. + move=> /braid_abaP[a [b [Heq ->{b1} ->{b2}]]]. rewrite !big_cons !big_nil !mulg1 !mulgA. move: Heq => /orP[] /eqP Heq. * by rewrite -Heq; apply Hbraid; rewrite Heq. * by rewrite -Heq; symmetry; apply Hbraid; rewrite Heq. + move=> /braidCP[a [b [Heq ->{b1} ->{b2}]]]. rewrite !big_cons !big_nil !mulg1. move: Heq => /orP[] Heq. * by apply Hcom; rewrite Heq /=. * by symmetry; apply Hcom; rewrite Heq /=. - move=> /reducesP[a [l [b [->{c} ->{w0}]]]]. rewrite !big_cat /= !big_cons !big_nil !mulg1. have:= Hsq l (ltn_ord l); rewrite expgS expg1 => ->. by rewrite mul1g. exists (Morphism (in2W morph_eltrP)) => i Hi /=. rewrite /morph_eltr_fun; have /= -> := (canword_eltr (Ordinal Hi)). by rewrite big_seq1. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr