proposition: Lemma addd_div_le a b c : (a / c)%D + (b / c)%D <= (a + b) / c.
proof: Proof. rewrite led_addE. apply/andP; split; apply: led_divl; [exact: led_addr|exact: led_addl]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice