def sub_le

stelliferous@0.0.2.0 · proofs/nat_order.bend:202

import stelliferous@0.0.2.0/proofs/nat_order.bend as NatOrder

import Base

202def sub_le(+a: Nat,+b: Nat) -> {Nat.is_le(Nat.sub(a,b),a) == True{} : Bool}:
203  match a b:
204    case 0n 0n:
205      {==}
206    case 0n 1n+b:
207      {==}
208    case 1n+ +a 0n:
209      reflexive(1n+a)
210    case 1n+ +a 1n+ +b:
211      successor(Nat.sub(a,b),a,sub_le(a,b))

Uses (6)

Used by (2)