Commit 2022-02-27 14:34 de721d3f

View on Github →

Fin n is a LinearOrder (#215) I'm not exactly sure whether this is the correct location? The change is pretty trivial to move wherever anyways.

Estimated changes

added theorem Fin.le_antisymm
added theorem Fin.le_refl
added theorem Fin.le_total
added theorem Fin.le_trans
added theorem Fin.lt_iff_le_not_le