proposition: Lemma product_neg (a b : R): a * b < 0 -> a != 0 /\ b != 0.
proof: Proof. case (eqVneq a 0) => [->|]; first by rewrite mul0r ltxx. case (eqVneq b 0) => [->|] //; by rewrite mulr0 ltxx. 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)