fact: Definition changes_minfty (p : seq {poly R}) := changes (map (fun p : {poly _} => (-1) ^+ (~~ odd (size p)) * lead_coef p) p).
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)