fact: Definition NPEadd e1 e2 := match e1, e2 with | PEc c1, PEc c2 => PEc (c1 + c2) | PEc c, _ => if (c =? 0)%coef then e2 else e1 + e2 | _, PEc c => if (c =? 0)%coef then e1 else e1 + e2 | _, _ => (e1 + e2) end%poly.
imports: ZArith_base