proposition: Lemma led_div a b c d : a <= b -> d <= c -> a / c <= b / d.
proof: Proof. move=> Hab Hcd; rewrite -mul_div_equiv. apply/(le_trans _ Hab); rewrite mul_div_equiv. exact: led_divr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice