def maximum_left

stelliferous@0.0.2.0 · proofs/nat_extrema.bend:50

import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

50def maximum_left(+left: Nat,+right: Nat) -> {Nat.is_le(left,Nat.max(left,right)) == True{} : Bool}:
51  match left right:
52    case 0n right: Order.zero_le(right)
53    case 1n+ +left 0n: Order.reflexive(left)
54    case 1n+left 1n+right: maximum_left(left,right)