proposition: Lemma sub_seqpoly_0 (s : seqpoly) : s - 0 = s.
proof: Proof. by elim: s. 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)