ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁, m₂)
⊢ denote_le ctx (cancel m₁ m₂)
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁, m₂)
⊢ denote_le ctx (cancel m₁ m₂)
simp
case h
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁, m₂)
⊢ denote_le ctx (List.reverse [] ++ m₁, List.reverse [] ++ m₂)
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁, m₂)
⊢ denote_le ctx (cancel m₁ m₂)
apply denote_le_cancelAux
no goals
case h
ctx : Context
m₁ m₂ : Poly
h : denote_le ctx (m₁, m₂)
⊢ denote_le ctx (List.reverse [] ++ m₁, List.reverse [] ++ m₂)
simp [h]