proposition: Lemma mul_div_equiv a b x : (x * a <= b) = (x <= b / a).
proof: Proof. apply/idP/idP => H; [exact: set_join_ub|]. by move: (div_mul_le b a); apply/le_trans/led_mul2r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice