proposition: Lemma mule_ge0_le0 x y : 0 <= x -> y <= 0 -> x * y <= 0.
proof: Proof. by move=> x0 y0; rewrite muleC mule_le0_ge0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed