proposition: Lemma schangei_reca a l n: a != 0 -> ((all_ss a l) = (SIA l n a == [::])).
proof: Proof. move => anz; move: n; elim: l => [// | b l h n]. by rewrite /= (negbTE anz)/= (h n.+1) ltNge; case sab: (0 <= b * a). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol