no goals
ctx : Context
cs : Certificate
h : PolyCnstr.denote ctx (combine cs) → False
⊢ denote ctx cs
match cs with
| [] => simp [combine, PolyCnstr.denote, Poly.denote_eq] at h
| (k, c)::cs =>
  simp [denote, combine] at *
  intro h'
  apply of_combineHyps (h := h)
  simp [h']
no goals
ctx : Context
cs : Certificate
h : PolyCnstr.denote ctx (combine []) → False
⊢ denote ctx []
simp [combine, PolyCnstr.denote, Poly.denote_eq] at h
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c)) cs) → False
⊢ ExprCnstr.denote ctx c → denote ctx cs
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combine ((k, c) :: cs)) → False
⊢ denote ctx ((k, c) :: cs)
simp [denote, combine] at *
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c)) cs) → False
h' : ExprCnstr.denote ctx c
⊢ denote ctx cs
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c)) cs) → False
⊢ ExprCnstr.denote ctx c → denote ctx cs
intro h'
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c)) cs) → False
h' : ExprCnstr.denote ctx c
⊢ PolyCnstr.denote ctx (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c))
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c)) cs) → False
h' : ExprCnstr.denote ctx c
⊢ denote ctx cs
apply of_combineHyps (h := h)
no goals
ctx : Context
cs✝ : Certificate
k : Nat
c : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c)) cs) → False
h' : ExprCnstr.denote ctx c
⊢ PolyCnstr.denote ctx (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c))
simp [h']