Notations for equality, order, and comparisons

This is a preliminary summary of notations used in different libraries for equality and orders, to bool, or to Prop, or to sumbool, or to comparison.

Please extend / complete with any information you may have.

Library	Order to Prop	equality/order to bool	equality/order to {x=y}+{x<>y}	comparison to comparison	Remarks
Stdlib	lt, le / <, <=	eqb, ltb, leb / =?, <?, <=?	eq_dec, lt_dec, le_dec	compare / ?=	for each type / with some inconsistencies
ExtLib	lt, lte / <., <=.	lt_dec, lte_dec / <!, <=!	lt_dec_p, lte_dec_p / <?, <=?		generic class notations
MathComp		lt, le / <, <=
TLC	lt, le / <, <=				generic class notations

Apparently no particular notations in stdpp, math-classes.

Other remarks:

• Coq's stdlib have various other schemes such as eq_decidable for equality to x=y \/ x<>y. Sometimes eq_bool to bool. Also trichotomy.
• Ternary notations such as x < y < z seem common in various libraries.