proposition: Lemma seqn0_size (s: seq R) : (s`_(size s).-1 != 0) -> (0 < size (seqn0 s))%N.
proof: Proof. move=> Hs. have Hssize : (0 < size s)%N. case: s Hs => [ | ] //=. by rewrite eqxx. elim: s Hs Hssize => [|a] //=. case=> [_ Ha _ | b l IHbl Hln Hablsize ] //=. by rewrite Ha. case Ha : (a != 0) => //. by apply: IHbl. 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)