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