proposition: Lemma prodNsimpl_ge (a b x: R): b * a < 0 -> 0 <= x * b -> x * a <= 0.
proof: Proof. move => pa; move: (square_pos (proj1 (product_neg pa))) => pb. by rewrite - (nmulr_lle0 _ pa) mulrA - (mulrA _ _ b) mulrAC pmulr_lle0. 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)