proposition: Lemma le_anti_dioid : antisymmetric le_dioid.
proof: Proof. by move=> a b /andP[]; rewrite /le => /eqP ? /eqP; rewrite addrC => <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop ssralg)