proposition: Lemma seqn0_n : forall (s : seq R), s`_(size s).-1 != 0 -> (seqn0 s)`_(size (seqn0 s)).-1 = s`_(size s).-1.
proof: Proof. move=> s 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. have H2 : (size [::a, b & l]).-1 = (size (b ::l)).-1.+1. by rewrite prednK. rewrite H2 /= -IHbl //. case Ha : (a != 0) => //. have H3 : ((size (a :: (if b != 0 then b :: seqn0 l else seqn0 l))).-1 = (size (seqn0 (b :: l))).-1.+1). by rewrite prednK // seqn0_size. by rewrite H3. 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)