proposition: Lemma schange_simpl (a b x: R): b * a < 0 -> 0 <= x * b -> x * a <= 0.
proof: Proof. move => pa. rewrite - (nmulr_lle0 _ pa) mulrA - (mulrA _ _ b) mulrAC pmulr_lle0 //. by rewrite lt0r sqr_ge0 sqrf_eq0 (proj1 (product_neg pa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol