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