proposition: Lemma schange_index_correct l (i: nat): i \in (schange_index l) -> (l`_i != 0 /\ l`_i * (0::l)`_i <= 0).
proof: Proof. move: {2 3} (schange_index l) (refl_equal (schange_index l)); case => //. have aux: forall i l n a, i \in SIA l n a -> exists2 j:nat, j \in SIA l 0 a & i = (j + n)%N. by move => i' l' n a; rewrite -(add0n n) schangei_addm; move /mapP. move => k s /schangei_snn [l1 [a [l2 [-> anz il1 l1z sv]]]]. rewrite inE; case/ orP. move /eqP ->; rewrite !nth_cat il1 ltnn subnn /=; split => //. rewrite -cat_cons nth_cat /= ltnS leqnn -last_nth. suff : (last 0 l1 == 0) by move => /eqP ->; rewrite mulr0. by move: (mem_last 0 l1); rewrite inE => /orP; case => //; move /(allP l1z). rewrite - sv => isv. move : (aux i l2 (size l1).+1 a isv) => [j j2 j1]. rewrite j1 addnC nth_cat - cat_cons nth_cat addSn - addnS ltnNge leq_addr /=. rewrite addnC addnK /= addSn ltnNge ltnS leq_addl /= -addnS addnK. move: j2; clear il1 l1z isv j1 sv k s l1 l i. move: {1} 0%N {1} (SIA l2 0 a) (refl_equal (SIA l2 0 a)) => n s. move:s l2 a n j anz; elim. by move => l2 a n j _; rewrite -(add0n n) schangei_addm; case (SIA l2 0 a). move => a s Hrec l b n j bnz => eq1;symmetry in eq1. move: (schangei_recc bnz eq1)=> [l1 [c [l3 [pa pb cz pc [pd pe]]]]] => js. have: (j + n)%N \in SIA l n b. by rewrite-{2} (add0n n) schangei_addm; apply /mapP; exists j. rewrite eq1 in_cons => /orP []. rewrite pd addnC eqn_add2l => /eqP ->. rewrite pa - cat_cons nth_cat ltnn subnn; split => //. rewrite /= - (cat_cons) nth_cat /= ltnS leqnn -last_nth. move: (mem_last b l1)=> /orP;case; first by move/eqP => ->;apply: ltW. by rewrite mulrC; move/(allP pc); apply schange_simpl; rewrite mulrC. rewrite - pe - addnS (addnC n) schangei_addm; move /mapP. move => [j0 ka] /eqP; rewrite eqn_add2r => /eqP => ->. move: ka; rewrite -(add0n (size l1).+1) schangei_addm => /mapP [k jv ->]. symmetry in pe; move: (Hrec l3 c (n + size l1).+1 k cz pe jv). rewrite pa - cat_cons ! nth_cat - addSnnS leqNgt ltnS leq_addl /=. by rewrite addnK /= addSnnS leqNgt ltnS leq_addl /= addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol