proposition: Lemma schange_index_tail l i s : schange_index l = rcons s i -> exists l1 a l2, [/\ l = l1 ++ a :: l2, (i <= size l1)%N, 0 < a * l`_i & all_eq0 l2].
proof: Proof. move => /schange_index_tail2 [l1 [a [l2 [-> pa pb pc]]]]. have:has (fun z => z != 0) (a::l2) by rewrite /= pa. move /has_split_eq_rev => [la [b [lb [qa qb qc]]]]. exists (l1 ++ la),b, lb. rewrite pb size_cat leq_addr nth_cat ltnn subnn /= qa catA; split => //. rewrite lt0r (mulf_neq0 qb pa) /=. have: b \in a :: l2 by rewrite qa mem_cat mem_head orbT. rewrite in_cons =>/orP []; first by move /eqP => ->; rewrite sqr_ge0. by move /(allP pc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol