def nat.le_trans

bend-osdev-algo@0.1.0.0 · PROOF.bend:947

import Base

947def nat.le_trans(a: Nat, b: Nat, c: Nat, e: {Nat.is_le(a, b) == True{} : Bool}, f: {Nat.is_le(b, c) == True{} : Bool}) -> {Nat.is_le(a, c) == True{} : Bool}:
948  match a b c:
949    case 0n _ _:
950      nat.le_zero(c)
951    case 1n+ap 0n _:
952      Empty.absurd({Nat.is_le(1n+ap, c) == True{} : Bool}, absurd.ft(e))
953    case 1n+ap 1n+bp 0n:
954      Empty.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, absurd.ft(f))
955    case 1n+ap 1n+bp 1n+cp:
956      nat.le_trans(ap, bp, cp, e, f)