proposition: Lemma prodsK w : 's_[w] * 's_[rev w] = 1.
proof: Proof. Proof using. elim/last_ind: w => [| w wn IHw] /=. by rewrite /rev /= !big_nil mulg1. rewrite rev_rcons -cat1s -cats1 -big_cat /=. rewrite -catA -[wn :: rev w]cat1s [X in w ++ X]catA cat1s !big_cat /=. suff -> : 's_[[:: wn; wn]] = 1 by rewrite mul1g. by rewrite big_cons big_seq1 eltr2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr