proposition: Lemma schangei_recc a l i s n: a!= 0 -> SIA l n a = i :: s -> exists l1 b l2, [/\ l = l1 ++ b :: l2, b *a <0, b!= 0, (all_ss a l1) & (i = n+size l1)%N /\ SIA l2 (n + size l1).+1 b = s].
proof: Proof. move => anz;case alz: (all_ss a l). by move: alz; rewrite (schangei_reca _ n anz) => /eqP ->. move: (negbT alz); rewrite - (has_predC) => /has_split [l1 [b [l2 [-> pb pc]]]]. move: pb => /=; rewrite - ltNge => abn. case bz: (b!=0); last by move: abn; rewrite (eqP (negbFE bz)) mul0r ltxx. have pc': all_ss a l1 by apply /allP => t /(allP pc) /= /negbNE. rewrite (schangei_recb l2 n abn pc') => /eqP h. by exists l1,b, l2; move: h; rewrite eqseq_cons => /andP [/eqP <- /eqP ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol