fact: Fixpoint PmulC_aux (P:Pol) (c:C) : Pol := match P with | Pc c' => Pc (c' *! c) | Pinj j Q => mkPinj j (PmulC_aux Q c) | PX P i Q => mkPX (PmulC_aux P c) i (PmulC_aux Q c) end.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory