proposition: Lemma drop1_seqn0_C : forall (s : seq R), (s`_0 != 0) -> drop 1 (seqn0 s) = seqn0 (drop 1 s).
proof: Proof. case=> [ | a l Ha] //=. by rewrite Ha /= !drop0. 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)