proposition: Lemma mul_divA a b c : a * (b / c)%D <= (a * b) / c.
proof: Proof. rewrite -mul_div_equiv -mulrA; exact/led_mul2l/div_mul_le. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice