case nil
ι : Type ?u.58476
α : Type ?u.58479
M : Type u_1
N : Type ?u.58485
P : Type ?u.58488
M₀ : Type ?u.58491
G : Type ?u.58494
R : Type ?u.58497
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
h : prod [] ≠ 1
⊢ 0 < length []

case cons
ι : Type ?u.58476
α : Type ?u.58479
M : Type u_1
N : Type ?u.58485
P : Type ?u.58488
M₀ : Type ?u.58491
G : Type ?u.58494
R : Type ?u.58497
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a head✝ : M
tail✝ : List M
h : prod (head✝ :: tail✝) ≠ 1
⊢ 0 < length (head✝ :: tail✝)
ι : Type ?u.58476
α : Type ?u.58479
M : Type u_1
N : Type ?u.58485
P : Type ?u.58488
M₀ : Type ?u.58491
G : Type ?u.58494
R : Type ?u.58497
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
L : List M
h : prod L ≠ 1
⊢ 0 < length L
cases L
case nil
ι : Type ?u.58476
α : Type ?u.58479
M : Type u_1
N : Type ?u.58485
P : Type ?u.58488
M₀ : Type ?u.58491
G : Type ?u.58494
R : Type ?u.58497
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
h : ¬0 < length []
⊢ ¬prod [] ≠ 1
case nil
ι : Type ?u.58476
α : Type ?u.58479
M : Type u_1
N : Type ?u.58485
P : Type ?u.58488
M₀ : Type ?u.58491
G : Type ?u.58494
R : Type ?u.58497
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
h : prod [] ≠ 1
⊢ 0 < length []
contrapose h
no goals
case nil
ι : Type ?u.58476
α : Type ?u.58479
M : Type u_1
N : Type ?u.58485
P : Type ?u.58488
M₀ : Type ?u.58491
G : Type ?u.58494
R : Type ?u.58497
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
h : ¬0 < length []
⊢ ¬prod [] ≠ 1
simp
no goals
case cons
ι : Type ?u.58476
α : Type ?u.58479
M : Type u_1
N : Type ?u.58485
P : Type ?u.58488
M₀ : Type ?u.58491
G : Type ?u.58494
R : Type ?u.58497
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a head✝ : M
tail✝ : List M
h : prod (head✝ :: tail✝) ≠ 1
⊢ 0 < length (head✝ :: tail✝)
simp