fact: Fixpoint poly_mul pl {struct pl} := match pl with | Cst cl => poly_mul_cst cl | Poly pl il ql => fun pr => let qs := poly_mul ql pr in if decide (null qs) then poly_mul pl pr else poly_add (poly_mul pl pr) (poly_mul_mon il qs) end.
imports: Bool PArith DecidableClass Ring Lia