proposition: Lemma seqmul_spseq_dropp : mid q = seqmul spseq (drop 1 p).
proof: Proof. apply: (@eq_from_nth _ 0) => [ | k Hk]. by rewrite mid_size seqmul_size spseq_size size_drop p_size subn1 minnE subKn. rewrite mid_coef_1 // q_k //. rewrite seqmul_coef. by rewrite nth_drop addnC addn1 spseq_coef // -mid_size. by rewrite spseq_size size_drop p_size subn1 minnE subKn // -mid_size. by rewrite -(@addn1 k) addnC -ltn_subRL subn1 -mid_size. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)