proposition: Lemma led_divr a b c : a <= b -> c / b <= c / a.
proof: Proof. move=> Hab; rewrite -mul_div_equiv. exact/(le_trans (led_mul2l _ Hab))/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