proposition: Lemma mul_div_le a b : a <= (a * b) / b.
proof: Proof. exact/set_join_ub/lexx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice