def by_contra

bend-kit-collections@0.1.4.1 · nat_order.bend:233

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

233# Proves x <= y from a refutation of y < x.
234def by_contra(x: Nat, y: Nat, k: LE(1n+y, x) -> Empty) -> LE(x, y):
235  match x y:
236    case 0n y:
237      MNat.zero_le(y)
238    case 1n+xp 0n:
239      Empty.absurd(LE(1n+xp, 0n), k(MNat.zero_le(xp)))
240    case 1n+xp 1n+yp:
241      by_contra(xp, yp, k)