proposition: Lemma reduced_revE w : (w \is reduced) = (rev w \is reduced).
proof: Proof. Proof using. apply/idP/idP; first exact: reduced_rev. by move/reduced_rev; rewrite revK. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr