fact: Fixpoint mon_of_pol (P:Pol) : option (C * Mon) := match P with | Pc c => if (c ?=! cO) then None else Some (c, mon0) | Pinj j P => match mon_of_pol P with | None => None | Some (c,m) => Some (c, mkZmon j m) end | PX P i Q => if Peq Q P0 then match mon_of_pol P with | None => None | Some (c,m) => Some (c, mkVmon i m) end else None end.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory