ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : Poly.denote_le ctx (Poly.cancel (toNormPoly a) (toNormPoly b)) = Poly.denote_le ctx (toNormPoly a, toNormPoly b)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)
have := Poly.denote_le_cancel_eq ctx a.toNormPoly b.toNormPoly
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : Poly.denote_le ctx (toPoly c, toPoly d) = Poly.denote_le ctx (toNormPoly a, toNormPoly b)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : Poly.denote_le ctx (Poly.cancel (toNormPoly a) (toNormPoly b)) = Poly.denote_le ctx (toNormPoly a, toNormPoly b)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)
rw [h] at this
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : (denote ctx c ≤ denote ctx d) = (denote ctx a ≤ denote ctx b)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : Poly.denote_le ctx (toPoly c, toPoly d) = Poly.denote_le ctx (toNormPoly a, toNormPoly b)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)
simp [toNormPoly, Poly.norm,Poly.denote_le] at this
no goals
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : (denote ctx c ≤ denote ctx d) = (denote ctx a ≤ denote ctx b)
⊢ (denote ctx a ≤ denote ctx b) = (denote ctx c ≤ denote ctx d)
exact this.symm