proposition: Lemma reduces_catl u v w : reduces u v -> reduces (u ++ w) (v ++ w).
proof: Proof. Proof using. move/reducesP => [x] [i] [y] [-> ->]. by apply/reducesP; exists x, i, (y ++ w); rewrite -!catA. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr