def mod_small

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:320

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/lib/lemmas/proofs/natural_division.bend as ND

320def mod_small(+a: Nat, +n: Nat, +h: {Nat.is_lt(a, n) == True{} : Bool}) -> {Nat.mod(a, n) == a : Nat}:
321  match n:
322    case 0n:
323      Empty.absurd({Nat.mod(a, 0n) == a : Nat}, N.lt_zero_absurd(a, h))
324    case 1n+ +np:
325      ND.remainder(0n, np, a, N.lt_succ_le(a, np, h))