# Order on tropical algebraic structure #

This file defines the orders induced on tropical algebraic structures by the underlying type.

## Main declarations #

`ConditionallyCompleteLattice (Tropical R)`

`ConditionallyCompleteLinearOrder (Tropical R)`

## Implementation notes #

The order induced is the definitionally equal underlying order, which makes the proofs and constructions quicker to implement.

instance
instConditionallyCompleteLinearOrderTropical
{R : Type u_1}
[ConditionallyCompleteLinearOrder R]
: