fact: Fixpoint NPEmul (x y : PExpr C) {struct x} : PExpr C := match x, y with | PEc c1, PEc c2 => PEc (c1 * c2) | PEc c, _ => if (c =? 1)%coef then y else if (c =? 0)%coef then 0 else x * y | _, PEc c => if (c =? 1)%coef then x else if (c =? 0)%coef then 0 else x * y | e1 ^ n1, e2 ^ n2 => if (n1 =? n2)%N then (NPEmul e1 e2)^^n1 else x * y | _, _ => x * y end%poly.
imports: ZArith_base