proposition: Lemma schangei_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 => h. suff [l1 [a [l2 [-> pa pb pc]]]]: exists l1 (a : R) l2, [/\ l = l1 ++ a :: l2, a != 0, i = size l1 & all_ss a l2]. 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 => //. have: b \in a :: l2 by rewrite qa mem_cat mem_head orbT. rewrite lt0r (mulf_neq0 qb pa) /= in_cons =>/orP []; last by move /(allP pc). by move /eqP => ->; rewrite sqr_ge0. move: h;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 _]]]] h. suff [l0 [b [l3 [-> qb -> qd]]]]: exists l0 b l3, [/\ l2 = l0 ++ b :: l3, b !=0, i = ((size l1).+1 + size l0)%N & all_ss b l3 ]. by exists (l1++a::l0),b,l3; rewrite - catA cat_cons addSnnS size_cat //=. move: l2 a pb (size l1).+1 h; clear; elim: s. move => l b bnz n /= 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 b bnz n. 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(polydiv polyorder path interval polyrcf)