Lemmas about integer division needed to bootstrap omega
. #
dvd #
*div zero #
div equivalences #
mod zero #
ofNat mod #
mod definitiions #
mod equivalences #
/
ediv #
emod #
theorem
Int.emod_negSucc
(m : Nat)
(n : Int)
:
Int.negSucc m % n = Int.subNatNat n.natAbs (m % n.natAbs).succ
properties of /
and %
#
Equations
- x✝.decidableDvd x = decidable_of_decidable_of_iff ⋯