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