proposition: Lemma schangei_rec a l1 l2 n: a != 0 -> all_ss a l1 -> SIA (l1++l2) n a = SIA l2 (n + size l1)%N a.
proof: Proof. move => anz; move: n; elim : l1;first by move =>n /=; rewrite addn0. move =>b l hrec n /= /andP [pa pb]. by rewrite ltNge pa (negbTE anz) /= (hrec _ pb) addnS addSn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol