def dvd

bend-collections-laws-math@1.0.0.0 · spec/math/natural.bend:94

import Base

94# d divides a: a quotient k with a == k d (Mathlib's Dvd on Nat)
95def dvd(+d: Nat, +a: Nat) -> Type:
96  Sigma<&1, &1, Nat, k => {a == Nat.mul(k, d) : Nat}>