fact: Fixpoint norm_aux (pe:PExpr) : Pol := match pe with | PEO => Pc cO | PEI => Pc cI | PEc c => Pc c | PEX j => mk_X j | PEadd (PEopp pe1) pe2 => (norm_aux pe2) -- (norm_aux pe1) | PEadd pe1 (PEopp pe2) => (norm_aux pe1) -- (norm_aux pe2) | PEadd pe1 pe2 => (norm_aux pe1) ++ (norm_aux pe2) | PEsub pe1 pe2 => (norm_aux pe1) -- (norm_aux pe2) | PEmul pe1 pe2 => (norm_aux pe1) ** (norm_aux pe2) | PEopp pe1 => -- (norm_aux pe1) | PEpow pe1 n => Ppow_N (fun p => p) (norm_aux pe1) n end.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory