proposition: Lemma poly_shiftI {p} : poly_mult [0; 1] p ≃ (0 :: p).
proof: Proof. rewrite /poly_mult => i /=. rewrite poly_add_nthP /=. have ->: nth i (map (fun=> 0) p) 0 = 0. { by elim: i p => [|i IH] [|? p] /=. } move: i => [|i] /=; first done. rewrite poly_add_nthP. have ->: nth i [0] 0 = 0. { by move: i => [|[|i]]. } elim: i p => [|i IH] [|? p] /=; by [|lia]. Qed.
imports: List PeanoNat Lia Permutation Undecidability.SetConstraints.FMsetC Undecidability.PolynomialConstraints.LPolyNC Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun