proposition: Lemma reduced_catr u v : u ++ v \is reduced -> v \is reduced.
proof: Proof. Proof using. rewrite !unfold_in size_cat => /eqP H. have {H} Huv : length 's_[u] + length 's_[v] = size u + size v. apply/eqP; rewrite eqn_leq (leq_add (length_prods u) (length_prods v)) /=. by have:= lengthM 's_[u] 's_[v]; rewrite -big_cat /= H => ->. by have:= leq_addE (length_prods u) (length_prods v) Huv => [] [_ ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr