proposition: Lemma lte_nmull x y : y \is a fin_num -> y < 0 -> (y < x * y) = (x < 1).
proof: Proof. by move=> yfin y0; rewrite muleC lte_nmulr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed