package coq-mathcomp-dioid

Definitions of the algebraic structure of dioid following the style of ssralg in the Mathcomp library.

The main algebraic structures defined are:

• semirings: rings without oppositve for the additive law
• dioids: idempotent semirings (i.e., forall x, x + x = x)
• complete dioids: dioids whose canonical order (x <= y wen x + y = y) yields a complete lattice
• commutative variants (multiplicative law is commutative)

More details can be found in comments at the beginning of each file.