def ge_le

stelliferous@0.0.2.0 · proofs/nat_order.bend:225

import Base

225def ge_le(+a: Nat,+b: Nat) -> {Nat.is_ge(a,b) == Nat.is_le(b,a) : Bool}:
226  match a b:
227    case 0n 0n:
228      {==}
229    case 0n 1n+b:
230      {==}
231    case 1n+a 0n:
232      {==}
233    case 1n+a 1n+b:
234      ge_le(a,b)