~/jendhub

def internal_div_le_succ_r

bend-mathlib@0.8.1.0 · nat.bend:823

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

823def internal_div_le_succ_r(j: Nat, d: Nat, h: {True{} == Nat.is_le(j, d) : Bool}) -> {True{} == Nat.is_le(j, 1n+d) : Bool}:
824  match j d:
825    case 0n _:
826      {==}
827    case 1n+i 0n:
828      Empty.absurd({True{} == Nat.is_le(1n+i, 1n) : Bool}, internal_div_true_ne_false(h))
829    case 1n+i 1n+e:
830      internal_div_le_succ_r(i, e, h)

Uses (5)

Used by (1)