no goals
ctx : Context
p : Poly
h : isNonZero [] = true
⊢ denote ctx [] > 0
contradiction
case inl
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : k > 0
⊢ denote ctx p + k * Var.denote ctx v > 0

case inr
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : ¬(v == fixedVar) = true
h : isNonZero p = true
⊢ denote ctx p + k * Var.denote ctx v > 0
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
h : isNonZero ((k, v) :: p) = true
⊢ denote ctx ((k, v) :: p) > 0
by_cases he : v == fixedVar <;> simp [he, isNonZero] at h ⊢
case inl
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : k > 0
⊢ k + denote ctx p > 0
case inl
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : k > 0
⊢ denote ctx p + k * Var.denote ctx v > 0
simp [eq_of_beq he, Var.denote]
case inl.h
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : k > 0
⊢ succ 0 ≤ k + denote ctx p
case inl
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : k > 0
⊢ k + denote ctx p > 0
apply Nat.lt_of_succ_le
no goals
case inl.h
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : (v == fixedVar) = true
h : k > 0
⊢ succ 0 ≤ k + denote ctx p
exact Nat.le_trans h (Nat.le_add_right ..)
case inr
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : ¬(v == fixedVar) = true
h : isNonZero p = true
ih : denote ctx p > 0
⊢ denote ctx p + k * Var.denote ctx v > 0
case inr
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : ¬(v == fixedVar) = true
h : isNonZero p = true
⊢ denote ctx p + k * Var.denote ctx v > 0
have ih := of_isNonZero ctx h
no goals
case inr
ctx : Context
p✝ : Poly
k : Nat
v : Var
p : List (Nat × Var)
he : ¬(v == fixedVar) = true
h : isNonZero p = true
ih : denote ctx p > 0
⊢ denote ctx p + k * Var.denote ctx v > 0
exact Nat.le_trans ih (Nat.le_add_right ..)