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