Skip to content
Rainbow docs menu

Reference · Natural numbers

rainbow.math.nat.divisibility

Natural numberssrc/rainbow/math/nat/divisibility.clj1 definitions, 0 theorems

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

DefinitionSource, line 21

nat/divides :
  (x₁ x₂ : ℕ)
  → Prop

ℕ = data/Nat