~/jendhub

def internal_div_mono_wit

bend-mathlib@0.8.1.0 · nat.bend:850

import bend-mathlib@0.8.1.0/nat.bend as Nat
import Base

850def internal_div_mono_wit(+a: Nat, +c: Nat, b: Nat, w: &k:Nat -> {Nat.add(a, k) == c : Nat}) -> le(Nat.div(a, 1n+b), Nat.div(c, 1n+b)):
851  match w:
852    case (+k, e):
853      %e : le(Nat.div(a, 1n+b), Nat.div(_, 1n+b))
854      Equal.sym(Bool, True{}, Nat.is_le(Nat.div(a, 1n+b), Nat.div(Nat.add(a, k), 1n+b)), internal_div_mono_go(a, b, 0n, 0n, k))

Uses (10)

Used by (1)