proposition: Lemma add_1d : @left_zero D D 1%O +%R.
proof: Proof. by move=> x; rewrite addrC add_d1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(fintype ssrnat bigop ssralg boolp classical_sets) dioid complete_lattice