feat(Algebra/Free): add length_pos lemma for free magmas (#11783)

This adds a `length_pos` lemma for multiplicative and additive free magmas. 

Indeed, it sometimes happens in proofs that we need to know that the length of any element is indeed strictly positive.

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))