proposition: Lemma seqn0_cons (s : seq R) (a : R) : (a != 0) -> seqn0 (a :: s) = a :: (seqn0 s).
proof: Proof. move=> Ha; by rewrite /= Ha. 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)