proposition: Lemma schange_index_tail2 s i l: schange_index l = rcons s i -> exists l1 (a : R) l2, [/\ l = l1 ++ a :: l2, a != 0, i = size l1 & all_ss a l2].
proof: Proof. case: s. move /schangei_snn => [l1 [a [l2 [ -> pb pc pd pe]]]]; exists l1, a, l2. by split => //; move: pe => /eqP; rewrite -schangei_reca. move => j s; move /schangei_snn => [l1 [a [l2 [-> pb pc _]]]]. move /(schange_index_tail1 pb) => [l0 [b [l3 [-> qb -> qd]]]]. exists (l1++a::l0),b,l3; rewrite - catA cat_cons addSnnS size_cat //=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol