proposition: Lemma schangei_recb a l1 b l2 n: b * a < 0 -> all_ss a l1 -> SIA (l1++ b::l2) n a = (n+size l1)%N :: SIA l2 (n + size l1).+1 b.
proof: Proof. move => h1 h2; move : (product_neg h1) => [bz az]. by rewrite (schangei_rec _ _ az h2) /= bz h1 orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol