fact: Fixpoint pcomp n (p : poly n) k (ps : vector (poly k) n) : poly k := match p with | nil => nil | cons (c,m) p' => cpmult c (mcomp m ps) + pcomp p' ps end.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia)