def dml

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natlight.bend:19

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR

19def dml(+x: Nat, +D: Nat, +hD: {Nat.is_lt(0n, D) == True{} : Bool}) -> {Nat.is_lt(Nat.mod(x, D), D) == True{} : Bool}:
20  match D:
21    case 0n:
22      Empty.absurd({Nat.is_lt(Nat.mod(x, 0n), 0n) == True{} : Bool}, N.lt_zero_absurd(0n, hD))
23    case 1n+ +dp:
24      NR.dm_lt(dp, x)