@[irreducible]
def
Nat.div.inductionOn
{motive : Nat → Nat → Sort u}
(x y : Nat)
(ind : (x y : Nat) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
(base : (x y : Nat) → ¬(0 < y ∧ y ≤ x) → motive x y)
:
motive x y
An induction principle customized for reasoning about the recursion pattern of natural number division by iterated subtraction.
Equations
- Nat.div.inductionOn x y ind base = if h : 0 < y ∧ y ≤ x then ind x y h (Nat.div.inductionOn (x - y) y ind base) else base x y h
Instances For
@[extern lean_nat_div_exact]
Division of two divisible natural numbers. Division by 0
returns 0
.
This operation uses an optimized implementation, specialized for two divisible natural numbers.
This function is overridden at runtime with an efficient implementation. This definition is the logical model.
Examples:
Nat.divExact 21 3 (by decide) = 7
Nat.divExact 0 22 (by decide) = 0
Nat.divExact 0 0 (by decide) = 0
Instances For
def
Nat.mod.inductionOn
{motive : Nat → Nat → Sort u}
(x y : Nat)
(ind : (x y : Nat) → 0 < y ∧ y ≤ x → motive (x - y) y → motive x y)
(base : (x y : Nat) → ¬(0 < y ∧ y ≤ x) → motive x y)
:
motive x y
An induction principle customized for reasoning about the recursion pattern of Nat.mod
.
Equations
- Nat.mod.inductionOn x y ind base = Nat.div.inductionOn x y ind base