proposition: Corollary lengthKR s t u : length (s * t * u) = length s + length t + length u -> length (t * u) = length t + length u.
proof: Proof. move=> Hstu. apply: lengthME; rewrite leqNgt; apply/negP => Habs. have:= lengthM s (t * u). rewrite mulgA Hstu -addnA leq_add2l => /(leq_trans Habs). by rewrite ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr