proposition: Lemma schange_index_tail1 s i l n a: a !=0 -> SIA l n a = rcons s i -> exists l1 b l2, [/\ l = l1 ++ b :: l2, b !=0, i = (n + size l1)%N & all_ss b l2 ].
proof: Proof. move: l n a; elim:s. move => l n b bnz /= h. move: (schangei_recc bnz h)=> [l1 [c [l2 [-> pa cz pb [pc pd]]]]]. by exists l1,c,l2; split => //; move:pd => /eqP; rewrite - schangei_reca. move => a l Hrec l2 n b bnz;rewrite rcons_cons. move /(schangei_recc bnz) => [l1 [c [l3 [-> pa cz pb [pc]]]]]. move /(Hrec _ _ _ cz) => [l0 [d [l4 [-> qa -> qc]]]]. by exists ( l1 ++ c :: l0), d,l4; rewrite -catA cat_cons addSnnS size_cat addnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol