cases xs with | mk xvars =>
apply xvars.recOnList (motive:=λ xvars => degree deg ⟨xvars⟩ = 0 → FreeCMonoid.mk xvars = 1)
case mk.nil => intros; rfl
case mk.cons =>
  intro a b xvars _ _ heq0
  rw [degree_cons] at heq0
  have : deg a * b.1 > 0 := Nat.mul_pos (hdeg_pos a) b.2
  have : deg a * b.val + degree deg ⟨xvars⟩ > 0 :=
    calc
      0 < deg a * b.val := Nat.mul_pos (hdeg_pos a) b.2
      _ ≤ deg a * b.val + degree deg ⟨xvars⟩ := Nat.le_add_right _ _
  rw [heq0] at this
  cases this
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
xs : FreeCMonoid α
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
⊢ degree deg xs = 0 → xs = 1
no goals