def modlt

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/misc.bend as MS
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL

623def modlt(+n: Nat, +V: Nat, +hne: {Nat.is_eq(V, 0n) == False{} : Bool}) -> {Nat.is_lt(Nat.mod(n, V), V) == True{} : Bool}:
624  match V:
625    case 0n:
626      Empty.absurd({Nat.is_lt(Nat.mod(n, 0n), 0n) == True{} : Bool}, FL.true_ne_false(hne))
627    case 1n+ +vp:
628      MS.divmod_lt(n, vp)