fact: Fixpoint reduce_aux k p := match p with | Cst c => Cst c | Poly p i q => if decide (i = k) then poly_add (reduce_aux k p) (reduce_aux k q) else let qs := reduce_aux i q in if decide (null qs) then (reduce_aux k p) else Poly (reduce_aux k p) i qs end.
imports: Bool PArith DecidableClass Ring Lia