proposition: Lemma seqn0_size_2 (s : seq R) : (s`_0 < 0) -> (0 < s`_(size s).-1) -> (1 < size (seqn0 s))%N.
proof: Proof. move=> Hs1 Hs2. have Hssize : (0 < size s)%N. case: s Hs1 Hs2 => [ | ] //=. by rewrite ltxx. case: s Hs1 Hs2 Hssize => [|a ] //. case=> [Ha1 Ha2 _ | b l Ha Hln Hablsize] //. have: false => //. rewrite -(lt_asym 0 a). by apply/andP. rewrite seqn0_cons /=. rewrite -(addn1 0) -(addn1 (size (seqn0 (b ::l)))) ltn_add2r seqn0_size //. have H : (size [:: a, b & l]).-1 = (size (b :: l)).-1.+1. by rewrite /=. rewrite H lt_def in Hln. by move/andP : Hln; case => -> _. rewrite lt_def eq_sym in Ha. by move/andP : Ha; case => ->. 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)