fact: Fixpoint boolean_witness p := match p with | Cst c => nil | Poly p i q => if decide (null p) then let var := boolean_witness q in list_replace var i true else let var := boolean_witness p in list_replace var i false end.
imports: Bool DecidableClass Algebra Ring PArith Lia