proposition: Lemma spec_aux_eq0 s : (s == 0)%C -> spec_seqpoly_aux 0 s = 0.
proof: Proof. elim: s=> [_|a s ih aseq0] //=. have heq0 : (a == 0)%C /\ (s == 0)%C. move: aseq0; rewrite /(_ == _)%C /eq_seqpoly /= => /andP [a0 s0]. split => //; rewrite /eq_op /eq_seqpoly sub_seqpoly_0. by rewrite s0. by rewrite (proj1 heq0) spec_aux_shift ih ?(proj2 heq0) // mul0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly polydiv) CoqEAL(hrel param refinements poly_op)