proposition: Lemma schange_sgr l: schange l = schange [seq sgr z | z <- l].
proof: Proof. rewrite /schange /filter0 filter_map; set s1 := [seq z <- l | z != 0]. set s := (filter (preim _ _)); have -> : s l = s1. apply: eq_in_filter => x xl /=. by rewrite sgr_def; case xz: (x!=0); rewrite ?mulr0n ?eqxx ?mulr1n ?signr_eq0. elim: s1 => [ // | a l1 /= ->]; case l1 => /=; first by rewrite !mulr0. by move => b l2; rewrite - sgrM sgr_lt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polydiv polyorder path interval polyrcf)