fact: Fixpoint PEsimp (e : PExpr C) : PExpr C := match e with | e1 + e2 => (PEsimp e1) ++ (PEsimp e2) | e1 * e2 => (PEsimp e1) ** (PEsimp e2) | e1 - e2 => (PEsimp e1) -- (PEsimp e2) | - e1 => NPEopp (PEsimp e1) | e1 ^ n1 => (PEsimp e1) ^^ n1 | _ => e end%poly.
imports: ZArith_base