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