proposition: Lemma bottom_zero : 0%O = 0%R :> D.
proof: Proof. by apply/le_anti; rewrite le0x le0d. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice