fact: Fixpoint coef n (m : monom n) (p : poly n) : Z := match p with | nil => 0 | cons (c,m') p' => match monom_eq_dec m m' with | left _ => c + coef m p' | right _ => coef m p' end end.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia)