proposition: Lemma div_mul_le a b : (a / b)%D * b <= a.
proof: Proof. by rewrite set_mulDr; apply: set_join_le_ub => y [z + <-]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice