Content created by Fredrik Bakke and Victor Blanchi.
Created on 2023-05-10.
Last modified on 2023-05-13.
The type of natural numbers equipped with its standard ordering relation forms a total order.
ℕ-Decidable-Total-Order : Decidable-Total-Order lzero lzero pr1 ℕ-Decidable-Total-Order = ℕ-Poset pr1 (pr2 ℕ-Decidable-Total-Order) n m = unit-trunc-Prop (linear-leq-ℕ n m) pr2 (pr2 ℕ-Decidable-Total-Order) = is-decidable-leq-ℕ
- 2023-05-13. Fredrik Bakke. Refactor to use infix binary operators for arithmetic (#620).
- 2023-05-10. Victor Blanchi. Fundamental theorem of arithmetic (#612).