Library BoundedNat.even_half
- Definition of even and its small inversion
- Small inversion for smaller inversion: half and its properties
- Smaller inversion to be used in richer functions such as even_rect
Library BoundedNat.looping_absurd
Library BoundedNat.bounded_nat
Library BoundedNat.bounded_even
This page has been generated by coqdoc