def transitive

stelliferous@0.0.2.0 · proofs/nat_order.bend:169

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

169def transitive(+a: Nat,+b: Nat,+c: Nat,ab: {Nat.is_le(a,b) == True{} : Bool},bc: {Nat.is_le(b,c) == True{} : Bool}) -> {Nat.is_le(a,
170    c) == True{} : Bool}:
171  match a:
172    case 0n:
173      zero_le(c)
174    case 1n+ +p:
175      match b:
176        case 0n:
177          Empty.absurd({Nat.is_le(1n+p,c) == True{} : Bool},WordEncoding.false_true(ab))
178        case 1n+ +q:
179          match c:
180            case 0n:
181              Empty.absurd({Nat.is_le(1n+p,0n) == True{} : Bool},WordEncoding.false_true(bc))
182            case 1n+r:
183              transitive(p,q,r,ab,bc)