Reference · Natural numbers
rainbow.math.nat.divisibility
Native natural-number divisibility for arithmetic proof interfaces. `nat/divides d n` is constructive evidence of a natural factor k with d*k = n. The definition is reducible, kernel-checked, and axiom-free on D63.
nat/divides
nat/divides : (x₁ x₂ : ℕ) → Prop
ℕ = data/Nat