proposition: Lemma reducedM (s t : 'S_(n.+1)) : length (s * t) = length s + length t -> canword s ++ canword t \is reduced.
proof: Proof. rewrite unfold_in big_cat /= size_cat -!size_canword => <-. by rewrite !canwordP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr