~/jendhub

def internal_div_gt_add

bend-mathlib@0.8.1.0 · nat.bend:902

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

902def internal_div_gt_add(a: Nat, +y: Nat) -> {False{} == Nat.is_le(1n+Nat.add(a, y), a) : Bool}:
903  match a:
904    case 0n:
905      {==}
906    case 1n+ap:
907      internal_div_gt_add(ap, y)

Uses (4)

Used by (1)