div_thm
⊢ ∀x y q r. x DIV y = if x = q * y + r ∧ r < y then q else x DIV y
mod_thm
⊢ ∀x y q r. x MOD y = if x = q * y + r ∧ r < y then r else x MOD y
num_case_compute_lazy
⊢ num_CASE = (λn f g. if n = 0 then f else g (PRE n))