def nodiv

bend-collections-laws-math@1.0.0.0 · spec/math/number.bend:65

import Base

65# no d in [d, d + k) divides n
66def nodiv(k: Nat, +n: Nat, +d: Nat) -> Bool:
67  match k:
68    case 0n:
69      True{}
70    case 1n+p:
71      Bool.and(Bool.not(Nat.is_eq(Nat.mod(n, d), 0n)), nodiv(p, n, 1n+d))