proposition: Lemma mule_gt0_lt0 x y : 0 < x -> y < 0 -> x * y < 0.
proof: Proof. rewrite lt_def !lt_neqAle => /andP[? ?]/andP[? ?]. by rewrite mule_neq0 ?mule_ge0_le0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed