proposition: Lemma gee_pmull y x : y \is a fin_num -> 0 < x -> y <= 1 -> y * x <= x.
proof: Proof. move: x y => [x| |] [y| |] _ //=. - by rewrite lte_fin => x0 r0; rewrite /mule/= lee_fin ger_pMl. - by move=> _; rewrite /mule/= eqe => r1; rewrite leey. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed