proposition: Lemma pmule_rge0 x y : 0 < x -> (x * y >= 0) = (y >= 0).
proof: Proof. move=> x_gt0; apply/idP/idP; last exact/mule_ge0/ltW. by apply: contra_le; apply: mule_gt0_lt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed