def pk.le_trans

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:88

import Base

88def pk.le_trans(+a: Nat, +b: Nat, +c: Nat) -> {Nat.is_le(a, b) == True{} : Bool} -> {Nat.is_le(b, c) == True{} : Bool} -> {Nat.is_le(a, c) == True{} : Bool}:
89  match a b c:
90    case 0n _ 0n:
91      h1 => h2 => {==}
92    case 0n _ 1n+cp:
93      h1 => h2 => {==}
94    case 1n+ap 0n _:
95      h1 => h2 => pk.absurd({Nat.is_le(1n+ap, c) == True{} : Bool}, h1)
96    case 1n+ap 1n+bp 0n:
97      h1 => h2 => pk.absurd({Nat.is_le(1n+ap, 0n) == True{} : Bool}, h2)
98    case 1n+ap 1n+bp 1n+cp:
99      h1 => h2 => pk.le_trans(ap, bp, cp)(h1)(h2)