- [x] `nat_of_pos`, `nat_of_bin`, `pos_of_nat`, and `bin_of_nat` (in `ssrnat.v`). - [ ] `fact_rec` and `factorial` (in `ssrnat.v`). - [ ] operators for finite ordinals (in `fintype.v`). - [ ] `prime`, `logn`, `pdiv`, `max_pdiv`, and `totient` (in `prime.v`). - [ ] `up_log` (in `prime.v`, available only from MathComp 1.14.0, see math-comp/math-comp#823). - [ ] `binomial_rec`, `binomial`, `ffact_rec`, and `falling_factorial` (in `binomial.v`). - [ ] `Order.min` and `Order.max` for `natdvd` (in `order.v`). - [ ] `Order.lteif` and `Order.leif` for `bool`, `nat`, `natdvd`, and `int` (in `order.v` and `ssrint.v`). - [ ] `exprz` for `int` (in `ssrint.v`). - [ ] operators for rational numbers (in `rat.v`).
nat_of_pos,nat_of_bin,pos_of_nat, andbin_of_nat(inssrnat.v).fact_recandfactorial(inssrnat.v).fintype.v).prime,logn,pdiv,max_pdiv, andtotient(inprime.v).up_log(inprime.v, available only from MathComp 1.14.0, see adding logarithm truncate up math-comp#823).binomial_rec,binomial,ffact_rec, andfalling_factorial(inbinomial.v).Order.minandOrder.maxfornatdvd(inorder.v).Order.lteifandOrder.leifforbool,nat,natdvd, andint(inorder.vandssrint.v).exprzforint(inssrint.v).rat.v).