proposition: Lemma nmule_rle0 x y : x < 0 -> (x * y <= 0) = (y >= 0).
proof: Proof. by rewrite -oppe_gt0 => /pmule_rge0<-; rewrite mulNe oppe_ge0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed