fact: Fixpoint poly_mul_mon k p := match p with | Cst c => if decide (null p) then p else Poly (Cst false) k p | Poly p i q => if decide (i <= k)%positive then Poly (Cst false) k (Poly p i q) else Poly (poly_mul_mon k p) i (poly_mul_mon k q) end.
imports: Bool PArith DecidableClass Ring Lia