fact: Fixpoint PsubC (P:Pol) (c:C) : Pol := match P with | Pc c1 => Pc (c1 -! c) | Pinj j Q => Pinj j (PsubC Q c) | PX P i Q => PX P i (PsubC Q c) end.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory