proposition: Lemma le_trans_dioid : transitive le_dioid.
proof: Proof. move=> a b c; rewrite /le_dioid => /eqP baa /eqP <-. by rewrite -[in X in _ == X]baa addrA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop ssralg)