diff --git a/Mathlib/Algebra/Free.lean b/Mathlib/Algebra/Free.lean
index 18dec944d1738..8c286e41d9482 100644
--- a/Mathlib/Algebra/Free.lean
+++ b/Mathlib/Algebra/Free.lean
@@ -328,6 +328,13 @@ def FreeAddMagma.length {α : Type u} : FreeAddMagma α → ℕ
 
 attribute [to_additive existing (attr := simp)] FreeMagma.length
 
+/-- The length of an element of a free magma is positive. -/
+@[to_additive "The length of an element of a free additive magma is positive."]
+lemma FreeMagma.length_pos {α : Type u} (x : FreeMagma α) : 0 < x.length :=
+  match x with
+  | FreeMagma.of _ => Nat.succ_pos 0
+  | mul y z => Nat.add_pos_left (length_pos y) z.length
+
 /-- Associativity relations for an additive magma. -/
 inductive AddMagma.AssocRel (α : Type u) [Add α] : α → α → Prop
   | intro : ∀ x y z, AddMagma.AssocRel α (x + y + z) (x + (y + z))