proposition: Lemma lte_nmul2l z : z \is a fin_num -> z < 0 -> {mono *%E z : x y /~ x < y}.
proof: Proof. rewrite -oppe0 lteNr => zfin z0 x y. by rewrite -(oppeK z) !mulNe lteNl oppeK -2!mulNe lte_pmul2l ?fin_numN. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed