proposition: Lemma product_neg (a b : R): a * b < 0 -> a != 0 /\ b != 0.
proof: Proof. move => h. case bz: (b!=0); last by move: h; rewrite (eqP (negbFE bz)) mulr0 ltxx. case az: (a!=0); last by move: h; rewrite (eqP (negbFE az)) mul0r ltxx. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype order) mathcomp(binomial bigop ssralg poly ssrnum ssrint rat) mathcomp(polyrcf) pol