fact: Fixpoint valid_dec k p := match p with | Cst c => true | Poly p i q => negb (decide (null q)) && decide (i < k)%positive && valid_dec i p && valid_dec (Pos.succ i) q end.
imports: Bool PArith DecidableClass Ring Lia