proposition: Lemma spec_aux_eq0 p : eq0_hpoly p -> spec_hpoly_aux 0%N p = 0.
proof: Proof. elim: p=> [c|c m p ih] /=; first by move->. move/andP=> heq0. by rewrite (proj1 heq0) (proj2 heq0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) CoqEAL(param refinements pos hrel poly_op)